_posts/2018-11-10-popl19.md

+---
+title: Papers accepted at POPL 2019
+---
+
+Congratulations to José Fragoso Santos, Philippa Gardner, Petar Maksimović, 
+Martin Bodin and Gaby Sampaio, whose papers were accepted at this year’s 
+[ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019)](https://popl19.sigplan.org/home).
+
+José, Petar, Gaby and Philippa had their paper ['JaVerT 2.0: Compositional 
+Symbolic Execution for JavaScript']({{site.baseurl}}{% link publications/FragosoSantos2019JaVerT.html %}) accepted. The paper describes JaVerT 2.0, 
+a symbolic analysis tool for JavaScript that follows the language semantics 
+without simplifications. 
+
+Martin and Philippa's paper, written in collaboration with 
+[Thomas Jensen](http://www.irisa.fr/celtique/jensen/) and 
+[Alan Schmitt](http://people.rennes.inria.fr/Alan.Schmitt/), 
+from [Inria]( https://www.inria.fr/en/centre/rennes), is ['Skeletal Semantics 
+and Their Interpretations']({{site.baseurl}}{% link publications/Bodin2019Skeletal.html %}) and in it, they introduce a skeletal semantics of 
+a language, where each skeleton describes the complete semantic behaviour of 
+a language construct. You can find more details and additional proofs on the [companion page](http://skeletons.inria.fr/popl2019/index.html)
+and their [artifact on their Gitlab repository](https://gitlab.inria.fr/skeletons/Coq/tree/POPL2019).
\ No newline at end of file

_posts/2018-11-7-facebook.md

+---
+title: Facebook Continuous Reasoning research award for JaVerT 2.0.
+---
+
+Philippa Gardner, Jose Fragoso Santos and Petar Maksimovic have won a [Facebook 
+Continuous Reasoning research award](https://research.fb.com/announcing-the-winners-of-the-facebook-continuous-reasoning-research-awards/) 
+for their project JaVerT 2.0: Automatic Compositional Analysis for JavaScript.  
+
+[JaVerT 2.0](https://www.doc.ic.ac.uk/~pg/publications/FragosoSantos2019JaVerT.pdf) 
+is a separation-logic-based tool for JavaScript analysis and testing that follows 
+the language semantics without simplifications. It supports whole-program symbolic 
+testing, verification, and automatic compositional testing based on bi-abduction.
+The award, one of five awarded on the call, was open to research teams working on 
+[applying formal methods using continuous reasoning and in particular, those addressing 
+fundamental problems for mostly-automatic or interactive verifiers.](https://research.fb.com/programs/research-awards/proposals/continuous-reasoning-research-award/)
\ No newline at end of file

_posts/2019-04-01-eccop2019.md

+---
+title: Paper accepted at ECOOP 2019
+---
+
+Congratulations to Petar Maksimović and Philippa Gardner, whose paper with 
+[Conrad Watt](https://www.cl.cam.ac.uk/~caw77/) and [Neel Krishnaswami](https://www.cl.cam.ac.uk/~nk480/)
+(University of Cambridge) has been accepted at this year’s [European Conference 
+on Object-Oriented Programming (ECOOP '19)](https://2019.ecoop.org/)
+
+In their paper: [“A Program Logic for First-Order Encapsulated WebAssembly”](https://2019.ecoop.org/event/ecoop-2019-papers-a-program-logic-for-first-order-encapsulated-webassembly) 
+they introduce Wasm Logic, a sound program logic for first-order, encapsulated 
+WebAssembly. Using Wasm Logic, they also specify and verify a simple WebAssembly 
+tree library, giving abstract specifications independent of the underlying implementation. 
+You can [read the draft submitted for publication here](https://www.cl.cam.ac.uk/~nk480/wasm-pl.pdf).
\ No newline at end of file

_posts/2019-05-1- fMfSS_talk.md

+---
+title: Talk at Formal Methods for Statistical Software workshop, Martin Bodin
+---
+[Martin Bodin](https://vtss.doc.ic.ac.uk/people/bodin.html) gave a talk “A Trustworthy Mechanized Formalization of R“ at the 
+[Formal Methods for Statistical Software (FMfSS 2019)](https://samate.nist.gov/FMSwVRodeo/FMfSS2019.html) 
+workshop, to present his work on big-step operational semantics for R.  The abstract for the talk is below. 
+
+The FMfSS workshop aims to identify formal methods, tools, and techniques that 
+can be used to gain higher assurance of statistical software. The workshop is 
+co-located with the [High Confidence Software and Systems Conference](https://cps-vo.org/group/hcss_conference) 
+and is organised by the U.S. Census Bureau and the [National Institute of Standards and Technology (NIST)]( https://www.nist.gov/)
+
+Abstract: The R programming language is very popular for developing statistical 
+software and data analysis, thanks to rich libraries, concise and expressive syntax, 
+and support for interactive programming. Yet, the semantics of R is fairly complex, 
+contains many subtle corner cases, and is not formally specified. This makes 
+it difficult to reason about R programs.
+In this work, we develop a big-step operational semantics for R in the form of 
+an interpreter written in the Coq proof assistant. We ensure the trustworthiness 
+of the formalization by introducing a monadic encoding that allows the Coq interpreter, 
+CoqR, to be in direct visual correspondence with the reference R interpreter, 
+GNU R. Additionally, we provide a testing framework that supports systematic 
+comparison of CoqR and GNU R. In its current state, CoqR covers the nucleus 
+of the R language as well as numerous additional features, making it pass 
+a significant number of realistic test cases from the GNU R and FastR projects. 
+To exercise the formal specification, we prove in Coq the preservation 
+of memory invariants in selected parts of the interpreter. 
+This work is an important first step towards a robust environment for 
+formal verification of R programs.
\ No newline at end of file

_posts/2019-05-13-lorentz _seminar.md

+---
+title: Effective Verification Workshop at the Lorentz centre, talks by Philippa Gardner and Emanuele D’Osualdo
+---
+
+Philippa Gardner and Emanuele D'Osualdo gave invited talks as this May's Lorentz centre workshop: 
+[Effective Verification: Static Analysis Meets Program Logics]( http://lorentzcenter.nl/lc/web/2019/1115/description.php3?wsid=1115&venue=Snellius) in Leiden, The Netherlands.
+
+Philippa gave a talk on TADA Live: Compositional Reasoning for the Termination 
+of Fine-grained Concurrent Programs and Emanuele gave a talk entitled: Inductive 
+Invariants for Automatic Verification of Cryptographic Protocols.
+
+The [Lorentz Center workshop series](http://lorentzcenter.nl/progsel.php) 
+brings together scientists in a work environment that fosters exchange and 
+interaction and the establishment of collaborations. For the [Effective 
+Verification workshop](http://lorentzcenter.nl/lc/web/2019/1115/description.php3?wsid=1115&venue=Snellius), 
+the centre invited researchers in both static analysis and program logics 
+(e.g. concurrent separation logic) and encouraged them to share each other's 
+techniques and tools. The goal is to help promote work developing more effective 
+automation for program logics (using techniques from static analysis), as well 
+as help extend static analysis to prove more daring properties beyond safety 
+(using techniques from program logics).
+ 
+You can find the [programme of the workshop here](http://lorentzcenter.nl/lc/web/2019/1115/program.pdf)
+
+![Effective Verification Static Analysis Meets Program Logics poster](/images/posts/Lorentz.jpg)
\ No newline at end of file

_posts/2019-05-31-goodbye _andrea.md

+---
+title: Goodbye to Dr Andrea Cerone
+---
+
+Our very best wishes to Andrea Cerone, who after three years with the group is 
+leaving to take up a position as a software engineer for [Footballradar](https://www.footballradar.com/).
\ No newline at end of file

_posts/2019-06-03-calco.md

+---
+title: 8th Conference on Algebra and Coalgebra in Computer Science
+---
+Philippa Gardner and Emanuele D’Osualdo are part of the local organising team for 
+[the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)](https://www.coalg.org/calco-mfps-2019/calco/) 
+which is taking place in London this week. 
+
+CALCO aims to bring together researchers and practitioners with interests in 
+foundational aspects, and both traditional and emerging uses of algebra and coalgebra 
+in computer science. It takes place alongside the [35th Conference on the 
+Mathematical Foundations of Programming Semantics (MFPS 2019)](https://www.coalg.org/calco-mfps-2019/mfps/)
+
+[The conference programme](https://www.coalg.org/calco-mfps-2019/programme/) and [list 
+of accepted papers](https://www.coalg.org/calco-mfps-2019/calco/calco19-list-of-accepted-papers/) are now available from the [conference website](https://www.coalg.org/calco-mfps-2019/calco/). 

_posts/2019-07-26-srepls.md

+---
+title: Emanuele D'Osualdo and Shale Xiong, talks at Surrey Concurrency Workshop and S-REPLS
+---
+
+Emanuele D'Osualdo and Shale Xiong both gave talks at this year's [Surrey Concurrency Workshop 
+and S-REPLS](https://cw-srepls-19.github.io/#schedule).
+
+The two-day workshop, which was hosted by the [University of Surrey this year](https://cw-srepls-19.github.io/#previous), is aimed at 
+bringing together researchers working on the theory of concurrency and the 
+semantics and implementation of programming languages. 
+
+You can find the abstract for Emanuele’s talk on [TaDA Live](https://cw-srepls-19.github.io/abstracts.html#gardner)
+and Shale’s talk on [Data Consistency in Transactional Storage Systems](https://cw-srepls-19.github.io/abstracts.html#xiong) 
+on the [workshop page](https://cw-srepls-19.github.io/abstracts.html#gardner).
\ No newline at end of file

_posts/2019-08-09-marktoberdorf.md

+---
+title: Summer School Marktoberdorf 2019
+---  
+Gaby Sampaio and Sacha Ayoun, two of the group’s PhD students, were invited to 
+attend the [40th Marktoberdorf Summer School](https://www2.in.tum.de/mod19/index.html), 
+organised by the [Technical University of Munich (TUM)](https://www.tum.de/). 
+
+The Summer School Marktoberdorf is a 10-day course for young computer scientists 
+and mathematicians working on formal approaches to correctness and security of software systems. 
+This year’s topic was “Safety and Security for Software Systems: Logics, Proofs, 
+Applications” and the focus was on the latest verification tools developed to 
+mechanize the design of safe and secure programs. The busy programme, with lectures, 
+keynotes and presentations had a particular emphasis on Logics and Logical-based 
+Methods and mathematical reasoning about safety and security and protection against 
+failure, and also included sports days, socials and a visit to Neuschwanstein Castle.
+
+![One of the presentations during the summer school](/images/images/Marktoberdorf.jpg)
\ No newline at end of file

_posts/2019-08-15-jose.md

+---
+title: Goodbye to Jose Fragoso
+---
+
+Goodbye and good luck to Jose Fragoso, who is moving to the 
+[Instituto Superior Técnico, Lisbon, Portugal](https://tecnico.ulisboa.pt/pt/) 
+to become an Assistant Professor in the [Department of Computer Science and 
+Engineering](https://fenix.tecnico.ulisboa.pt/departamentos/dei/o-dei). 
+
+Jose will be conducting his research as part of the [SAT group](https://inesc-id.pt/group/II08/) 
+at the [INESC-ID]( https://inesc-id.pt/about-us/#).
\ No newline at end of file

_posts/2019-09-26-workshop.md

+---
+title: Workshop on Verified Software, Isaac Newton Institute for Mathematical Sciences, Cambridge.
+---
+Philippa Gardner was one of the organisers of the [`Verified Software’ 
+workshop](https://vetss.org.uk/vetss-verified-software-workshop-24th-25th-september-2019/), 
+held at the [Isaac Newton Institute for Mathematical Sciences, (INI)](http://www.newton.ac.uk/), 
+Cambridge on 24th-25th September 2019.
+
+The workshop was organised by [VeTSS, the Research Institute in Verified Trustworthy 
+Software Systems](https://vetss.org.uk/) working in partnership with the Newton 
+Gateway to Mathematics and the Isaac Newton Institute (INI). The two day workshop 
+is a forerunner to [the INI’s six-week summer programme on `Verified Software’ 
+in the summer of 2020](http://www.newton.ac.uk/event/vso).
+The programme of the two days, together with slides and videos of the talks can 
+be downloaded from the [workshop page](https://vetss.org.uk/verified-software-workshop-programme/).
+
+![Future Challenges Discussion with Tony Hoare, John Goodacre and Philippa Gardner](/images/posts/Verified-Software-Workshop.jpg)
\ No newline at end of file

_posts/2019-10-01-internship.md

+---
+title: Internship at Facebook, Infer Team
+---
+
+Julian Sutherland has just returned from a three months internship with the Facebook's Infer team. 
+
+While at Facebook, Julian worked to develop a static analysis tool for [Infer]( https://fbinfer.com/), 
+quandryBO, intended to statically find unchecked array accesses tainted by user-provided 
+information. He also worked on extending the capabilities of the current infer 
+buffer overflow analysis, InferBO and dealing with function calls within infer's 
+intermediate representation, SIL. 
+
+[Infer is a static analysis tool]( https://github.com/facebook/infer) for Java, 
+C++, Objective-C, and C which was [open-sourced in 2015]( https://engineering.fb.com/developer-tools/open-sourcing-facebook-infer-identify-bugs-before-you-ship/).
\ No newline at end of file

_posts/2019-10-28-iris.md

+---
+title: Talk at Iris Workshop, Aarhus University, Denmark
+---
+Philippa Gardner, Emanuele D’Osualdo and Julian Sutherland attended the first edition 
+of the [Iris workshop](https://iris-project.org/workshop-2019/#program).
+
+The two-day workshop, held at Aarhus University, Denmark focused on [Iris]( https://iris-project.org/), 
+a Higher-Order Concurrent Separation Logic Framework implemented and verified 
+in the proof assistant Coq that can be used for reasoning about safety of concurrent programs.
+
+Philippa gave a talk on their joint work on “Compositional Reasoning for the Termination of Fine-grained Concurrent Programs”.
\ No newline at end of file

_posts/2019-10-30-livestream.md

+---
+title: Facebook testing and verification symposium, 20-21 November, livestream
+---
+The [third annual Facebook testing and verification symposium](https://fbtavsymposium2019.splashthat.com/?gz=0949d2b64c045dc1ebb599012c988f37&pp=1&guest-access-hash=NDU3NDYzOTg2fDI2MzM0NTExOHwxNTcyMzg4MzY1OzYyMDc1MTc5MDZiODM5YjNiMzExNDA0ZTllNzUyNjhhZDlmNzk4OTk3N2RmMzZlMjY4Y2VmY2ZjYTE0YmI3MTI=) 
+will be held on 20-21 November in London. 
+
+This is a two-day programme of talks which aims to increase the collaboration 
+and exchange between testing and verification scientific research in academia 
+and industry.
+
+Many of the talks will be available to watch on livestream, for details see 
+the [event page](https://fbtavsymposium2019.splashthat.com/?gz=0949d2b64c045dc1ebb599012c988f37&pp=1&guest-access-hash=NDU3NDYzOTg2fDI2MzM0NTExOHwxNTcyMzg4MzY1OzYyMDc1MTc5MDZiODM5YjNiMzExNDA0ZTllNzUyNjhhZDlmNzk4OTk3N2RmMzZlMjY4Y2VmY2ZjYTE0YmI3MTI=).
\ No newline at end of file

_posts/2019-11-11- ini_workshop.md

+---
+title: Six week programme Verified Software at the Isaac Newton Institute, Cambridge
+---
+
+Philippa Gardner is one of the organisers of the [six week programme Verified 
+Software at the Isaac Newton Institute]( https://www.newton.ac.uk/event/vso
+), Cambridge. 
+
+The Verified Software programme includes two workshops, one on 
+the [Theory and Applications of Verified Software, From Theory to Practice](https://www.newton.ac.uk/event/vsow01) 
+and a second one on [Verification Tools and Experiments]( https://www.newton.ac.uk/event/vsow02). 
+These will be supplemented with smaller workshops and working groups devoted to specialized topics and industrial applications. 
+
+The aim of the programme is to bring together a diverse mix of 
+researchers to take stock of the first fifteen years of [Tony Hoare’s Verified 
+Software Challenge](https://www.researchgate.net/publication/221160548_Verified_Software_Theories_Tools_Experiments_Vision_of_a_Grand_Challenge_Project) 
+and formulate a concrete roadmap for international cooperation for the next fifteen years.
+
+Participation is by invitation only, but members of Cambridge University 
+are welcome to sign in as a non-registered attendee on the day(s) and attend 
+the lecture(s) and there are also [options to participate remotely}(https://www.newton.ac.uk/events/how-to-participate), 
+as most of the seminars at INI are streamed live and are made available for download as a webseminar shortly after the event.
\ No newline at end of file

_posts/2020-01-22-hase.md

+---
+title: Talk on Gillian, Workshop on High Assurance Systems Engineering, POPL2020
+---
+
+Philippa was one of the speakers at the [Interactive Knowledge 
+Shares session](https://popl20.sigplan.org/details/hase-2020-papers/2/Interactive-Knowledge-Shares) 
+of this year’s [HASE, the Workshop on High Assurance Systems Engineering]( https://popl20.sigplan.org/home/hase-2020)
+
+HASE, part of [POPL](https://popl20.sigplan.org), aims to bring about new collaborations 
+and launch shared initiatives to provide high levels of assurance about the correct operation and security properties 
+of production systems (software and hardware).
+
+Philippa presented Gillian, a language independent framework supporting 
+compositional symbolic analysis. Gillian supports three flavours of analysis: 
+whole-program symbolic testing, full verification, and bi-abduction. It comes with 
+fully parametric meta-theoretical results and a modular implementation, designed 
+to minimise the instantiation effort required of the user.
\ No newline at end of file

_posts/2020-02-20-shale.md

+---
+title: Congratulations to Dr Shale Xiong
+---
+
+Many congratulations to Shale Xiong, who very successfully defended his PhD thesis, [Parametric Operational Semantics
+for Consistency Models](https://vtss.doc.ic.ac.uk/publications/Xiong2020Parametric.html) today.
+
+Many thanks also to [Brijesh Dongol](https://www.surrey.ac.uk/people/brijesh-dongol), 
+[Annette Bieniusa](https://softech.informatik.uni-kl.de/homepage/de/staff/AnnetteBieniusa/) and [Susan Eisenbach](https://www.imperial.ac.uk/people/s.eisenbach)
+who acted as the examiners.
+
+Shale's thesis develops a novel operational semantics for distributed key-value stores.
+This model combines the evolution of a global multi-versioning view and the client-local partial views and the
+operational semantics allow to formulate consistency levels from read Strict Serializability to Read 
+Atomicity based on execution tests that validate the correctness of transactional operations on the shared data.  
+
+Shale is currently working as a Research Engineer in the Security group at [Arm Research, Cambridge](https://www.arm.com/resources/research)

_posts/2020-04-27-ecoop.md

+---
+title: Papers accepted at ECOOP 2020
+---
+
+Two papers by members of the group have been accepted at 
+the [34th European Conference on Object-Oriented Programming, ECOOP 2020](https://2020.ecoop.org/home).
+
+The paper by Gabriela, Jose, Petar and Philippa is entitled: [A Trusted Infrastructure 
+for Symbolic Analysis of Event-Driven Web Applications](https://2020.ecoop.org/track/ecoop-2020-papers#event-overview).
+
+It introduces a trusted infrastructure for symbolic analysis of modern event-driven Web applications. The infrastructure consists of reference implementations of the DOM Core Level 1 and UI Events, 
+JavaScript Promises, and the JavaScript async/await APIs, all underpinned by a simple 
+Core Event Semantics that is sufficiently expressive to describe the event models 
+underlying all these APIs. The implementations follow the API respective standards 
+line-by-line and have been thoroughly tested. An associated artifact was also 
+accepted by the evaluation committee.
+
+Shale, Andrea, Azalea and Philippa's paper, [Data Consistency in Transactional Storage Systems: 
+A Centralised Semantics](https://2020.ecoop.org/details/ecoop-2020-papers/21/Data-Consistency-in-Transactional-Storage-Systems-A-Centralised-Semantics), 
+presents an interleaving operational semantics for 
+describing the client-observable behaviour of atomic transactions 
+on distributed key-value stores.
+
+ECOOP is Europe’s longest-standing annual Programming Languages (PL) conference, bringing together researchers, 
+practitioners, and students working on all topics related to programming languages, 
+software development, object-oriented technologies, 
+systems and applications. All being well, this year's conference will take place in Berlin in July.
+
+Congratulations to all!
\ No newline at end of file

_posts/2020-05-11-pldi.md

+---
+title: Paper accepted at PLDI 2020
+---
+
+Congratulations to  Jose Fragoso, Petar Maksimovic, Sacha Ayoun and Philippa 
+Gardner, whose paper, [Gillian, Part I: A Multi-language Platform for Symbolic 
+Execution](https://vtss.doc.ic.ac.uk/publications/FragosoSantos2020Gillian.html), 
+has been accepted at this year’s PLDI.
+
+PLDI, the [ACM SIGPLAN Conference on Programming Language Design 
+and Implementation](https://pldi20.sigplan.org/) is one of the leading conferences 
+for practical and experimental work in the design and implementation of programming languages. 
+
+The conference was due to be held in London in 15-19 June 2020, but it is now to be held 
+virtually. Thanks to their sponsors, [attendance to the main 
+conference and co-located events will be free for registrations before the 
+5 June](https://pldi20.sigplan.org/attending/registration).
+
+
+

_posts/2020-05-19-thisispldi.md

+---
+title: PLDI 2020 song
+---
+
+This year’s PLDI has moved online and the organisers have 
+just [posted a song](https://pldi20.sigplan.org/news#%22This-is-Still-PLDI%22-song!) to 
+remind attendees that virtually or not, this is still PLDI. 
+
+You can check out the singing abilities of friends and colleagues, including our 
+own Philippa Gardner, [here](https://youtu.be/hVMCl64Uhe8). 
+
+PLDI 2020's technical program will run as a single track, 12 hours a day, from 
+Wednesday, 17 June through Friday, 19 June, with co-located events on Monday and 
+Tuesday, 15 and 16 June. 
\ No newline at end of file