_people/raad.md

@@ -7,8 +7,8 @@ email: azalea@imperial.ac.uk
 alumnus: true
 ---
 
-was a PhD student with the group, defending her thesis on [Abstraction, Refinement and Concurrent Reasoning]({{site.baseurl}}{% link publications/Raad2017Abstraction.html %}) in February 2017.
-She then moved to the [Max Planck Institute for Software Systems (Kaiserslautern)](https://www.mpi-sws.org/) 
+Azalea was a PhD student with the group, defending her thesis on [Abstraction, Refinement and Concurrent Reasoning]({{site.baseurl}}{% link publications/Raad2017Abstraction.html %}) in February 2017.
+She then moved to the [Max Planck Institute for Software Systems (Kaiserslautern)](https://www.mpi-sws.org/)
 working a postdoctoral researcher with [Derek Dreyer](https://people.mpi-sws.org/~dreyer/) and [Viktor Vafeiadis](https://people.mpi-sws.org/~viktor/)
-on the [ERC RustBelt project](http://plv.mpi-sws.org/rustbelt/). Azalea will join the faculty 
-at Imperial College London as a lecturer in 2020.
\ No newline at end of file
+on the [ERC RustBelt project](http://plv.mpi-sws.org/rustbelt/). In 2020, Azalea joined the faculty
+at Imperial College London as a lecturer.
\ No newline at end of file

_people/rao.md

+---
+firstname: Xiaojia
+lastname: Rao
+position: PhD Student
+webpage: 
+email: xiaojia.rao19@imperial.ac.uk
+github:  
+alumnus: false
+projects:
+  - gillian
+  - sl
+---
+
+Xiaojia is a PhD student at the Department of Computing at Imperial, under the supervision of Professor Philippa Gardner.
+
+Xiaojia studied for his BA and Math degree at the University of Cambridge and then moved to Imperial College London in 2020 to join the MSc in Advanced Computing. His Master's thesis was on a verified model of WebAssembly in Coq called WasmCert-Coq. He plans to expand this work, and also explore the Iris framework and [Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html) in his future research.
\ No newline at end of file

_people/sampaio.md

@@ -3,18 +3,13 @@ firstname: Gabriela
 lastname: Sampaio
 position: PhD Student
 webpage: https://www.doc.ic.ac.uk/~gcs817/
-email: g.sampaio17@imperial.ac.uk
+email:
 github:  
-alumnus: false
+alumnus: true
 projects:
   - web
   - moc
 ---
-Gabriela Sampaio is a PhD student at the [Department of Computing](http://www.doc.ic.ac.uk) at
+Gabriela Sampaio was a PhD student at the [Department of Computing](http://www.doc.ic.ac.uk) at
 Imperial, under the supervision of Professor Philippa Gardner. 
-She completed her BSc course at Federal University of Pernambuco (UFPE, Brazil) in 2015. 
-During the undergraduate course, she spent one year at the University of Kent, working on an Erlang refactoring project ([Wrangler](https://www.cs.kent.ac.uk/projects/wrangler/Wrangler/Home.html)) 
-under the supervision of Professor Simon Thompson. Later in 2017, she completed her MSc, also at UFPE, course under supervision of Professor Paulo Borba. 
-The work aims to support developers in partially safe changes to software product lines, with the use of a partial refinement theory. 
-The results were published at [SPLC'16](https://dl.acm.org/citation.cfm?id=2934482). Between the MSc and the PhD, Gabriela worked as a web developer in Brazil. 
-Her PhD thesis will focus on the reasoning and verification of large Javascript Programs.
+She completed her BSc  and MSc at Federal University of Pernambuco (UFPE, Brazil), spending a year abroad at the University of Kent, working on the Erlang refactoring project ([Wrangler](https://www.cs.kent.ac.uk/projects/wrangler/Wrangler/Home.html)). In 2022, Gabriela defended her PhD thesis, [A Trusted Infrastructure for Symbolic Analysis of Event based Web APIS](https://spiral.imperial.ac.uk/bitstream/10044/1/100397/1/CunhaSampaio-G-2022-PhD-Thesis.pdf), and took up a position at Meta (formerly Facebook).

_people/sutherland.md

@@ -3,12 +3,11 @@ firstname: Julian
 lastname: Sutherland
 position: PhD Student
 webpage: http://www.doc.ic.ac.uk/~jhs110/
-email: jhs110@doc.ic.ac.uk
-alumnus: false
+email: 
+alumnus: true
 projects:
   - concurrency
   - sl
 ---
 
-Julian is a PhD student with the group, currently working on extending 
-concurrent separational logics such as TaDA to a total correctness semantics (termination).
+Julian defended his PhD thesis, Compositional termination verification for fine-grained concurrency, in 2022. Julian is currently a Formal Verification Engineer at [Nethermind](https://nethermind.io/), a blockchain company working on Ethereum.

_people/wood.md

@@ -2,12 +2,9 @@
 firstname: Thomas
 lastname: Wood
 position: PhD Student
-webpage: http://www.doc.ic.ac.uk/~tw1509/
-email: tw1509@doc.ic.ac.uk
-github: edgemaster
+webpage: https://twitter.com/IgnoredAmbience
+github: IgnoredAmbience
 alumnus: true
-projects:
-  - web
 ---
 
-was a PhD student with the group, working on software automated testing, verification and reasoning techniques and theory.
\ No newline at end of file
+Thomas was a PhD student with the group, working on software automated testing, verification and reasoning techniques and theory.
\ No newline at end of file

_people/xiong.md

@@ -11,7 +11,6 @@ projects:
   - moc
 ---
 
-was a PhD student with the group. Shale defended his thesis: Parametric Operational 
-Semantics for Consistency Models in February 2020 and he is currently working 
-for [Arm Research]( https://www.arm.com/resources/research), Cambridge, as a 
-Research Engineer in their Security group.
\ No newline at end of file
+Shale was a PhD student with the group. Shale defended his thesis: [Parametric Operational 
+Semantics for Consistency Models](https://vtss.doc.ic.ac.uk/publications/Xiong2020Parametric.html) in February 2020 and he is currently working for [Arm Research](https://www.arm.com/resources/research), Cambridge, as a 
+Research Engineer in their Security group.

_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-04-27-ecoop20.md → _posts/2020-04-27-ecoop.md

@@ -5,7 +5,7 @@ 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 
+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, 
@@ -17,12 +17,11 @@ 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 novel interleaving operational semantics for 
+presents an interleaving operational semantics for 
 describing the client-observable behaviour of atomic transactions 
 on distributed key-value stores.
 
-ECOOP, the European Conference on Object-Oriented Programming, is Europe’s longest-standing annual 
-Programming Languages (PL) conference, bringing together researchers, 
+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.

_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

_posts/2020-06-16-advert.md

+---
+title: Post-doc Position(s) Available
+---
+
+There is an opening for at least one
+post-doctoral researcher in the Verified Software Group led by
+Professor Philippa Gardner. This position is initially
+for two years, with an option to extend in future. The funding from
+Philippa's EPSRC Fellowship allows for a flexible start date in
+these uncertain times, in the academic year starting September 2020.
+Further funding is expected to be available over the next year.  If
+interested, please contact [Philippa](mailto:p.gardner@imperial.ac.uk?subject=[Inquiry]%20Post-doctoral%20Position)
+directly as soon as possible.
+
+A successful candidate is likely to have a strong record of research
+in program analysis, testing, or verification. Former
+RAs and PhD students from the Verified Software group include
+Brotherston (UCL academic), Calcagno (Imperial academic, then
+Monoidics start-up, then Facebook), Maffeis
+(Imperial academic), Naudziuniene (Facebook Infer), Ntzik (Amadeus R&D),
+Raad (Imperial academic), Smith (Pivotal Software
+Inc.) and Villard (Facebook Infer). We have thriving interactions
+with the tech companies in London, especially Facebook and Amazon,
+who fund part of the group's research.
+
+Several potential projects are listed below, focussing on
+symbolic analysis, concurrency and distribution.
+
+### Gillian: a multi-language platform for compositional symbolic analysis
+
+The Verified Software Group has recently introduced
+[Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html) (PLDI'20),
+supporting three flavours of analysis: symbolic testing, full verification and
+automatic compositional testing, unified by a common symbolic
+execution engine that is parametric on the memory model of the target
+language. We instantiate Gillian to the real-world languages C and
+JavaScript, obtaining results on real-world code that demonstrate the
+viability of our unified, parametric approach.
+
+There are many possible projects. We would especially like to recruit
+someone interested in extending Gillian with concurrency or
+underpinning Gillian with Coq-certification.
+
+### Concurrency
+
+The Verified Software Group has worked on compositional reasoning about concurrent
+programs, introducing fundamental techniques underpinning modern
+concurrent separation logics: logical abstraction (CAP logic), logical
+atomicity (TaDA Safety) and logical environment liveness properties
+(TaDA Live). We have applied our reasoning to, for example, algorithms
+for manipulating concurrent B-trees, skip lists from
+java.util.concurrent, graph algorithms and the POSIX file system.
+
+There is still much to understand: for example, working with the
+fundamental theory; applying the work to real-world libraries;
+developing prototype analysis tools; or moving to the Coq-focused Iris
+project, which uses much of our foundational theory.
+
+### Distribution
+
+The Verified Software Group recently began to work on weak consistency models for
+distribution, developing an interleaving operational semantics for
+client-observational behaviour of atomic transactions (ECOOP’20).
+
+We would be interested in finding someone to work in this area: for example,
+developing further the operational semantics and providing prototype
+tools for proving robustness results or discovering litmus tests; or
+introducing program logics that connect with program logics for
+concurrency and weak memory.

_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

+---
+title: Paper accepted at CONCUR2020
+---
+
+Congratulations to [Emanuele D'Osualdo]( https://www.emanueledosualdo.com/) and [Felix Stutz](https://www.mpi-sws.org/people/fstutz/), whose paper, [Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions](https://drops.dagstuhl.de/opus/volltexte/2020/12843/pdf/LIPIcs-CONCUR-2020-31.pdf), has been accepted at this year’s [CONCUR]( https://concur2020.forsyte.at/).
+
+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, 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-01-manu.md

+---
+title: Goodbye to Emanuele D’Osualdo
+---
+
+Goodbye and our best wishes to Emanuele D’Osualdo, who is joining [Derek Dreyer]( https://people.mpi-sws.org/~dreyer/)'s group at the [Max Planck Institute for Software Systems (MPI-SWS)](https://www.mpi-sws.org/research-areas/programming-languages-and-verification/) in Saarbrücken, Germany in September. 
+
+Emanuele will be working on verification of concurrent programs and the [IRIS program logic](https://iris-project.org/).
\ No newline at end of file

_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