_posts/2020-10-01-rao.md

+---
+title: Welcome to Xiaojia Rao, new PhD student with the group
+---
+A very warm welcome to Xiaojia Rao who has just joined the group as a PhD student. 
+
+Xiaojia completed his BA and Math degree at the University of Cambridge in 2019 and then moved to Imperial College to do an MSc in Advanced Computing. His Master’s thesis, supervised by Philippa, was on a verified model of WebAssembly in Coq called WasmCert-Coq.
\ No newline at end of file

_posts/2020-11-04-codemeshtalk.md

+---
+title: Talk at Code Mesh, Philippa Gardner
+---
+
+Philippa will be one of the speakers at this year’s [Code Mesh](https://codesync.global/conferences/code-mesh-ldn/#Schedule), 
+a two-day conference on functional programming languages and alternative tech.  
+
+[The talk, on Gillian](https://codesync.global/speaker/philippa-a-gardner/), will give a general introduction to the multi-language platform for symbolic program analysis and its instantiation to JavaScript and C. 
\ No newline at end of file

_posts/2020-12-01-facetav.md

+---
+title: Fourth Facebook Testing and Verification Symposium (TAV), 1-3 December 2020
+---
+
+The [fourth Facebook Testing and Verification Symposium (TAV)](https://fbtavsymposium2020.bevylabs.com/events/details/facebook-tav-symposium-division-facebook-testing-and-verification-symposium-presents-facebook-testing-and-verification-symposium-2020/#/) will take place this week, with an interesting programme of speakers including our own Alastair Donaldson and Philippa Gardner. 
+
+TAV is conceived as an open environment for academia and industry to exchange ideas on testing and verification scientific research and practice. It is taking place virtually this year from the 1st  to 3rd Dec and is free to attend. 
+
+For more details, please see [this link to their blog post](https://research.fb.com/blog/2020/11/registration-now-open-for-the-2020-testing-and-verification-symposium/) this one to [the Facebook research page](https://research.fb.com/) or [the TAV group on Facebook](https://www.facebook.com/groups/FaceTAV/).

_posts/2021-01-12-gabi-internship.md

+---
+title: Internship at Amazon Web Services, Gabi Sampaio
+---
+
+Welcome back to Gabi Sampaio, who has just returned from a three-month 
+internship (albeit remotely) with the Prime Video Automated Reasoning team 
+at Amazon Web Services in London.
+
+The Prime Video team is part of their [Automated Reasoning Group (ARG)](https://www.amazon.science/latest-news/how-awss-automated-reasoning-group-helps-make-aws-and-other-amazon-products-more-secure) 
+which creates and implements automated reasoning tools to secure AWS’s 
+own infrastructure and services, as well as those of its customers.

_posts/2021-01-14-world-logic-day.md

+---
+title: UNESCO World Logic Day event
+---
+Philippa Gardner and Petar Maksimovic will take part in the [Computer Science needs Logic!](https://sites.google.com/view/imperial-worldlogicday2021/home) event, part of Imperial College contribution to the [UNESCO World Logic Day](https://en.unesco.org/commemorations/worldlogicday).
+
+The event, organised by Prof Alessandra Russo and Dr Mark Law, wants to 
+celebrate Logic as a vital and core part of Computing. The [programme](https://sites.google.com/view/imperial-worldlogicday2021/home/programme) will 
+showcase advancements made in "Logic and Programming Languages" 
+and "Logic and Artificial Intelligence", with presentations by PhD 
+students, post-docs and academics working in areas where there is a 
+need for logical inference or advantages in using logic-based methods. 
+
+Philippa will talk on “Compositional Reasoning about Software Systems: 
+Separation Logic.” and Petar with talk about “Gillian: A Multi-language 
+Platform for Compositional Symbolic Execution.”

_posts/2021-04-06-verified.md

+---
+title: Verified software workshops at the Newton institute, May and June
+---
+
+Philippa is one of the organisers of two upcoming workshops on Verification at the [Isaac Newton Institute for Mathematical Sciences]( https://www.newton.ac.uk/), in advance of their scientific programme on [Verified Software](https://www.newton.ac.uk/event/vso), which had to be postponed last summer.
+
+The two workshops: [Verified software: from theory to practice](https://www.newton.ac.uk/event/vsow03), to be held in May, and [Tools and Experiments](https://www.newton.ac.uk/event/vsow04) to be held in June, will be run virtually.  
+
+The workshops are intended for researchers working on the specification and verification of software-intensive systems, with a focus on work bridging the gap between theory and applications.   The Tools and Experiments workshop is aimed at defining an integrated tool resources for automated formal methods with standardized interfaces and it will include a special event marking the 60th anniversary of Tony Hoare's invention of Quicksort.

_posts/2021-04-15-collegedefrance.md

+---
+title: Talk at College de France, Philippa Gardner
+---
+
+Philippa Gardner gave a talk on [Gillian: a Multi-language Platform for Compositional Symbolic Analysis](https://www.college-de-france.fr/site/xavier-leroy/seminar-2021-04-15-11h15.htm) at the [College de France](https://www.college-de-france.fr/site/institution/Le-College-Presentation.htm), as part of their Program logic seminars.
+
+The talk was a  general introduction to [Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html), a multi-language platform for the development of symbolic-execution tools. Gillian currently supports three types of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. It uses a core symbolic execution engine with strong mathematical foundations that unifies bug catching and verification. So far, the Gillian team has instantiated Gillian to JavaScript and C, languages with substantially different memory models. These instantiations have been used: to find bugs in the real-world data-structure libraries Buckets.js and Collections-C; to find bugs and prove bounded correctness results for a real-world jQuery-like library, cash; and to verify the deserialisation function of the AWS Encryption SDK messaging system.
+
+The video of the talk is available [on this link](https://www.college-de-france.fr/site/xavier-leroy/seminar-2021-04-15-11h15.htm). 

_posts/2021-05-04-pldi21.md

+---
+title: PLDI21 official song and video now out
+---
+
+Another year, another PLDI conference, another excellent PLDI song and video: "Pure Implementation", displaying the musical talents of many friends and colleagues.  
+
+
+<iframe width="560" height="315" src="https://www.youtube.com/embed/77999Td20TM" title="YouTube video player" frameborder="0" allow="accelerometer; autoplay; clipboard-write; encrypted-media; gyroscope; picture-in-picture" allowfullscreen></iframe>
+
+
+PLDI is the ACM SIGPLAN Conference on Programming Language Design and Implementation, one of the premier conferences in the field of programming languages and programming systems research. The conference will be held virtually yet again this year, from Sunday 20 to Saturday 26 June 2021. [Registration is now open](https://pldi21.sigplan.org/).

_posts/2021-05-06-talk.md

+---
+title: Public Tech Talk on Gillian Verification of JavaScript and C, Galois
+---
+
+Philippa Gardner gave a public [live-stream](https://youtu.be/DqlC1tNElrg) technical talk on Gillian, Verification of JavaScript and C, hosted by [Galois](https://galois.com/about/). 
+
+The talk gave a general introduction to [Gillian](https://gillianplatform.github.io/), a platform for the development of symbolic-execution tools for many programming languages.
+
+Galois is a company specialising on applying [formal analysis techniques to the design of critical software systems](https://galois.com/research-development/). It runs a program of public [technical talks](https://galois.com/blog/category/tech-talks/), many of which are available online. 

_posts/2021-05-12-sampaio.md

+---
+title: Gabriela Sampaio, internship with the Static Analysis Tools team at Facebook London
+---
+
+Welcome (again) to Gabriela who has returned from her second industry internship, this time a three-months placement with the Static Analysis Tools team at Facebook London.
+
+The team develops [Infer](https://fbinfer.com), an static analysis tool that can find potential bugs in Java/C/C++/Objective-C code. During her internship at Facebook, Gabriela worked on porting [Pulse (an analyser developed as part of Infer)](https://fbinfer.com/docs/checker-pulse) to the Java programming language.

_posts/2021-05-31-cav21.md

+---
+title: Paper accepted at CAV 2021
+---
+
+Congratulations to Petar, Jose, Sacha and Philippa, whose paper and artifact have been accepted to CAV 2021, the [33rd International Conference on Computer-Aided Verification.](http://i-cav.org/2021/)
+
+In their paper, [Gillian, Part II: Real-World Verification for JavaScript and C](https://gitlab.doc.ic.ac.uk/resource-reasoning/publications/-/blob/696e94b1d2bd71031b6933ccac12561d36b38df6/Maksimovic2021Gillian.pdf), they introduce verification based on separation logic to [Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html), and their methodology for constructing compositional memory models for Gillian. They also verify the JavaScript and C implementations of the [AWS Encryption SDK](https://docs.aws.amazon.com/encryption-sdk/latest/developer-guide/introduction.html) message header deserialisation module, where they found two bugs in the JavaScript and three bugs in the C implementation.
+
+CAV is dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems and will be held online this year. 

_posts/2021-06-16-fm21.md

+---
+title: WebAssembly paper accepted
+---
+
+Congratulations to friends and colleagues [Conrad Watt]( https://www.cl.cam.ac.uk/~caw77/), [Xiaojia Rao](https://vtss.doc.ic.ac.uk/people/rao.html), [Jean Pichon-Pharabod](https://www.cl.cam.ac.uk/~jp622/), [Martin Bodin]( https://mbodin.github.io/index.html?pedanticJS=no) and Philippa Gardner, whose paper  [“Two mechanisations of WebAssembly 1.0”](https://gitlab.doc.ic.ac.uk/resource-reasoning/publications/-/blob/d7c1f1ee5690694acefb7f8836dda455ae309b05/Watt2021Two.pdf) has been accepted at the [24th International Symposium of Formal Methods (FM21).](http://lcs.ios.ac.cn/fm2021/)
+
+[WebAssembly (abbreviated Wasm)](https://webassembly.org/) is a new bytecode language supported by all major Web browsers, designed primarily to be an efficient compilation target for low-level languages such as C/C++ and Rust. Wasm is unusual in that it is officially specified through a formal semantics. The paper introduces two mechanised specifications of the WebAssembly 1.0 semantics, written in different theorem provers: WasmCert-Isabelle and WasmCert-Coq. Wasm's compact design and official formal semantics enables the mechanisations to be particularly complete and close to the published language standard. The paper presents a high-level description of the language's updated type soundness result, referencing both mechanisations and also describes the current state of the mechanisation of language features not previously supported: WasmCert-Isabelle includes a verified executable definition of the instantiation phase as part of an executable verified interpreter; WasmCert-Coq includes executable parsing and numeric definitions as on-going work towards a more ambitious end-to-end verified interpreter which does not require an OCaml harness like WasmCert-Isabelle.
+
+FM21, which was planned to take place at the Institute of Software, Chinese Academy of Sciences in Beijing, China on 20-26 2021, will in the end be held online this year. 

_posts/2021-07-02-toplas.md

+---
+title: Paper accepted at TOPLAS
+---
+Many congratulations to [Emanuele D’Osualdo](https://www.emanueledosualdo.com/about/), [Azadeh Farzan](https://www.cs.toronto.edu/~azadeh/), Philippa Gardner and [Julian Sutherland](https://www.doc.ic.ac.uk/~jhs110/), whose paper [“TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs”](https://gitlab.doc.ic.ac.uk/resource-reasoning/publications/-/blob/d7c1f1ee5690694acefb7f8836dda455ae309b05/DOsualdo2020TaDa.pdf) has been accepted for publication at the [ACM Transactions on Programming Languages and Systems (TOPLAS)](https://dl.acm.org/journal/toplas) journal. 
+
+The paper introduces TaDA Live, a separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The logic contributes several innovations to obtain modular rely/guarantee style reasoning for liveness properties and to blend them with logical atomicity. 
+
+TOPLAS is the bimonthly ACM peer-reviewed scientific journal on programming languages. TOPLAS reports in depth on recent research advances in the areas of programming languages. Papers published at TOPLAS must contain innovative and novel content that advances the state of the art of programming languages and systems; many congratulations to all on a fine achievement after a lot of hard work.

_posts/2021-08-14-ara.md

+---
+title: Amazon Research Award (ARA) to Philippa Gardner
+---
+
+Philippa Gardner has been announced as one of the recipients of the [Spring 2021 Amazon Research Awards (ARA)](https://www.amazon.science/research-awards).
+
+ARA is a program funding academic research to open-source projects by top academic researchers around the world. Philippa was one of 26 awards made to researchers from 25 universities in 11 countries. Her successful proposal: Gillian: A Multi-language Platform for Symbolic Testing and Verification, was funded as part of ARA's Amazon Web Services Automated Reasoning call. 
+
+[Daniel Kroening, senior principal scientist for the Automated Reasoning Group](https://www.amazon.science/author/daniel-kroening), welcomed the new ARA researchers. "Research in automated reasoning is deeply intertwined with a broad range of other research areas, touching machine learning, hardware and software engineering, robotics, and life sciences," he said "The 2021 Amazon Research Awards reflect this breadth, and the interdisciplinary nature of research that is necessary to take computing one step closer to that magic spark that drives human reasoning."   
+
+The proposed work, to instantiate Gillian with Rust and to test and verify some of the unsafe code in the standard Rust library, is part of the goal to develop Gillian into a robust platform for symbolic testing and verification, usable by specialist tool developers, professional code developers, and students.

_posts/2021-09-03-caroline.md

+---
+title: Welcome to Caroline Cronjager, visiting student
+---
+
+We are very happy to welcome Caroline Cronjager, a visiting student from Ruhr University Bochum, Germany.
+
+Caroline is a BSc Mathematics with Computer Science student from Ruhr-University Bochum, Germany. During the next three months she plans to
+work on incorrectness and under-approximating logic, starting off with soundness for under-approximate separation logic and will also be part of the team supporting students on the Scalable Software Verification course.  

_posts/2021-10-03-andreas.md

+---
+title: Welcome to Andreas Lööw, new researcher with the group
+---
+
+A very warm welcome to Andreas Lööw, who has just started with us as a Post-Doctoral researcher. 
+
+Andreas completed his PhD on [Building Verified Hardware and Verified Stacks in HOL](https://www.doc.ic.ac.uk/~aloow/papers/thesis.pdf) at Chalmers University of Technology, under the supervision of [Magnus Myreen](http://www.cse.chalmers.se/~myreen/). 
+
+[Andreas' research focuses on interactive theorem proving for software and hardware correctness](https://www.doc.ic.ac.uk/~aloow/) and much of his work revolves around trustworthy hardware; [his latest paper, on the development and verification of the Verilog synthesis tool Lutsig](https://dl.acm.org/doi/10.1145/3437992.3439916) was accepted at this year’s POPL’s [Certified Programs and Proofs (CPP)]( https://popl21.sigplan.org/home/CPP-2021?.) series.

_posts/2021-11-01-sacha_amazon.md

+---
+title: Sacha Ayoun, internship with Amazon Web Services
+---
+
+Welcome back to Sacha who has returned from a three-months internship with the CodeGuru team at Amazon Web Services.
+
+Amazon CodeGuru is a [set of publicly available developer tools](https://aws.amazon.com/codeguru/) that use machine learning to automatically review code for bugs and code quality and to suggest improvements.
+
+While at AWS, Sacha developed a proof of concepts analysis for Java that could help reduce the number of false positives or reduce the search space in other kinds of analyses without compromising soundness. Having enjoyed his time at AWS, he is planning to return for a second internship with them next year.

_posts/2021-11-05-his.md

+---
+title: Philippa Gardner, talk at High Integrity Software (HIS) conference
+---
+
+Philippa gave a talk on [Verified Trustworthy Software Specification](https://www.his-conference.co.uk/index.php?p=session/verified-trustworthy-software-systems) at this year's [High Integrity Software (HIS) Conference](https://www.his-conference.co.uk/).
+
+Now in its sixth year, [HIS](https://www.his-conference.co.uk/index.php?p=programme) aims to create a forum to share challenges, best practice and experience between software engineering practitioners. This year's HIS conference, under the theme: Assuring security and safety for critical software applications, focussed on cyber safety for embedded systems, innovations in testing and the application of formal methods to achieve cyber security.

_posts/2022-03-29-Gabi_viva.md

+---
+title: Congratulations to Dr Sampaio
+---
+
+Many congratulations to Gabriela Sampaio, who defended her PhD thesis, A Trusted Infrastructure for Symbolic Analysis of Event based Web APIS very succesfully today.
+
+Many thanks also to [Alan Schmitt](http://people.rennes.inria.fr/Alan.Schmitt/), [Frank Tip](http://www.franktip.org) and [Nicolas Wu](https://zenzike.com), who acted as the examiners.
+
+Gabriela's thesis presents her work developing a formal, executable semantics of a subset of the JavaScript programming language, including several key Application Program Interfaces (APIs) called [JaVerT.Click](https://github.com/javert-click/javert-click). The formalization models the Document Object Model (DOM) by which code executed in a browser interacts with the page that is being displayed, the JS promises and async/await mechanisms for asynchronous programming, and the WebMessaging and WebWorkers APIs for creating multiple workers that execute concurrently and communicate among each other using message-passing. The semantics can be instantiated to achieve either concrete or symbolic execution, enabling the construction of symbolic test cases that enable concise specification of tests that achieve good code coverage. 
+
+After a well deserved holiday, Gabriela will take up a position as a software engineer with Facebook London.

_posts/2022-04-04-rust.md

+---
+title: Talk at Rust Verification Workshop, ETAPS 2022
+---
+
+
+Sacha Ayoun and Petar Maksimovic gave a talk on Gillian-Rust: Unified Symbolic Analysis for Rust at the [Second Rust Verification Workshop (RW2022)](https://sites.google.com/view/rustverify2022/home), which was held in Munich, Germany, co-located with [ETAPS 2022](https://etaps.org/2022/)
+
+[Rust](https://www.rust-lang.org/) is a new programming language for writing performant code with strong type and memory safety guarantees, and a strong contender to becoming an alternative to C and C++ for systems programming. This has resulted in a growing interest in the program verification community for building program verifiers for Rust. 
+
+Following on from the first [Rust Verification Workshop in 2021](https://sites.google.com/view/rustverify2021/homes), this second workshop was aimed at language designers, application developers and formal verification tool builders, and intended as a forum for sharing research and build collaborations around developing verified Rust programs. Abstracts of the talks and slides will be avaible soon on the [Rust Verification Workshop](https://sites.google.com/view/rustverify2022/home).