_posts/2020-02-20-shale.md

@@ -2,8 +2,8 @@
 title: Congratulations to Dr Shale Xiong
 ---
 
-Many congratulations to Shale Xiong, who very successfully defended his PhD thesis, Parametric Operational Semantics
-for Consistency Models today.
+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)
@@ -14,4 +14,4 @@ This model combines the evolution of a global multi-versioning view and the clie
 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)
\ No newline at end of file
+Shale is currently working as a Research Engineer in the Security group at [Arm Research, Cambridge](https://www.arm.com/resources/research)

_posts/2020-06-16-deepspec.md

+---
+title: REMS and DeepSpec workshop, livestream talks
+
+---
+
+The [REMS+DeepSpec workshop](https://pldi20.sigplan.org/home/rems-deepspec-2020) 
+organized jointly by the [EPSRC project REMS: Rigorous Engineering for 
+Mainstream Systems (Cambridge, Imperial, and Edinburgh, UK)](https://www.cl.cam.ac.uk/~pes20/rems/) and the NSF 
+Expedition in Computing ["The Science of Deep Specification" (US)](https://deepspec.org/main) was held on Mon 15 - Tue 16 Jun 2020.
+
+The two-day  workshop, part of [PLDI 2020]( https://pldi20.sigplan.org/), combined in-depth presentations by members of the two projects with invited talks by external experts, 
+and general talks. The [program and list of talks 
+can be found here]( https://pldi20.sigplan.org/home/rems-deepspec-2020#program).
+
+You can also see the livestream of the talks for [Monday](https://www.youtube.com/watch?v=FnSIJqJM3DY) and [Tuesday](https://youtu.be/9Rt5-PeG_9A) on YouTube. Philippa’s talk, on [Gillian: a Multi-language Platform for Program Correctness and Incorrectness](https://pldi20.sigplan.org/details/rems-deepspec-2020/10/Gillian-a-Multi-language-Platform-for-Program-Correctness-and-Incorrectness) can be found on the link [here](https://youtu.be/9Rt5-PeG_9A?t=8087) or below from 2:14:50. 
+
+<iframe width="560" height="315" src="https://www.youtube.com/embed/9Rt5-PeG_9A" frameborder="0" allow="accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture" allowfullscreen></iframe>
\ No newline at end of file

_posts/2020-06-19-plditalk.md

+---
+title:  Video talk on Gillian at PLDI 2020
+---
+
+The talk by Petar Maksimovic on [Gillian: a Multi-language Platform for Program Correctness and Incorrectness](https://pldi20.sigplan.org/details/rems-deepspec-2020/10/Gillian-a-Multi-language-Platform-for-Program-Correctness-and-Incorrectness), presented at [PLDI 2020]( https://pldi20.sigplan.org/), is now available on the PLDI YouTube channel, and can be seen on the link [here]( https://youtu.be/TurhBym2leA) or below. 
+
+<iframe width="560" height="315" src="https://www.youtube.com/embed/TurhBym2leA" frameborder="0" allow="accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture" allowfullscreen></iframe>
\ No newline at end of file

_posts/2020-08-31-concur2020.md

@@ -6,6 +6,6 @@ Congratulations to [Emanuele D'Osualdo]( https://www.emanueledosualdo.com/) and
 
 The paper explores the limits of what security properties can be proven by automatic analyses and aims at developing algorithms for proving security properties of cryptographic protocols automatically. Cryptographic protocols underpin everything on the internet nowadays: their goal is to establish secure communication in an insecure channel, through the use of cryptography. Despite being ubiquitous, they are very tricky to design. Indeed hackers exploit flaws in deployed protocols every day, with huge costs for individuals and society at large. 
 
-In the paper, they develop a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the problem is undecidable in general, the authors introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Their core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Their invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness. They also provide a prototype implementation and report on its performance on some textbook examples. The [extended technical report](https://arxiv.org/abs/1911.05430) is also available on [this link](https://arxiv.org/abs/1911.05430).
+In the paper, the authors develop a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the problem is undecidable in general, the authors introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Their core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Their invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness. They also provide a prototype implementation and report on its performance on some textbook examples. The [extended technical report](https://arxiv.org/abs/1911.05430) is also available on [this link](https://arxiv.org/abs/1911.05430).
 
 CONCUR 2020, the [31st International Conference on Concurrency Theory](https://drops.dagstuhl.de/opus/portals/lipics/index.php?semnr=16161) will take place online on 1-4 September 2020.

_posts/2020-09-27-fellow.md

+---
+title: Congratulations to Philippa Gardner, elected Fellow of the RAEng 
+--- 
+
+Philippa was one of 53 engineers in the UK to be elected to the Fellowship of the Royal Academy of Engineering this year. 
+
+Becoming a [Fellow of the RAEng]( https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2020/fellows/professor-philippa-gardner) is one of the highest honors an engineer can receive in the UK, and it recognizes outstanding and continuing contributions to the profession. 
+
+After the announcement, Philippa expressed her hope that her work "will serve as a foundation for establishing trust in our modern software infrastructure” and thanked her the group, for what she described as a “real group achievement, not just my achievement"
\ No newline at end of file

_posts/2020-09-3-concurtalk.md

+---
+title: Video talk on Decidable Inductive Invariants at CONCUR 2020
+---
+
+The talk by Emanuele D’Osualdo and Felix Stutz on their paper ["Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions"](https://vtss.doc.ic.ac.uk/publications/DOsualdoS2020Decidable.html), presented at [CONCUR 2020](https://easychair.org/smart-program/CONCUR20/index.html), is now available online and can be seen [on the link here](https://youtu.be/h9fsG_vfeFw?t=1256) or below.
+
+<iframe width="560" height="315" src="https://www.youtube-nocookie.com/embed/h9fsG_vfeFw?start=1262" frameborder="0" allow="accelerometer; autoplay; encrypted-media; gyroscope; picture-in-picture" allowfullscreen></iframe>
\ No newline at end of file

_posts/2020-10-01-martin.md

+---
+title: Goodbye to Martin Bodin
+---
+
+Goodbye and our best wishes to Martin Bodin who is leaving the group to join [the Inria Grenoble-Rhône-Alpes Research Centre](https://www.inria.fr/en/centre-inria-grenoble-rhone-alpes), France, as a CRCN (chargé de recherche de classe normale) in the [Sound Programming of Adaptive Dependable Embedded Systems (Spades)](https://team.inria.fr/spades/) group.
+
+Ni deziras al vi bonŝancon en via nova posto ĉe Inria, Martin!
+
+The Spades group’s research focuses on component-based programming: analysis of embedded systems, both in term of correctness and efficiency (time or energy use) and Martin will work in particular on the topic of Skeletal Semantics as Certified Analyses of Real-world Programs. You can read more about his proposed research below.
+
+Many programming languages used in industry are complex. This complexity is sometimes associated to deep research questions, like pointer arithmetic or concurrency. However, this complexity is sometimes only due to special behaviours of these languages. Languages likes JavaScript or R are known for such unexpected special behaviours. Such programming languages are thus frequently idealised in research. This unfortunately narrows the application of formal analyses. My research aims at developing formalisms (namely, skeletal semantics in the context of the Coq proof assistant) that enable the application of analyses of such complex languages, in particular in the context of real-time systems.
\ No newline at end of file

_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.