_people/loow.md

+---
+firstname: Andreas
+lastname: Lööw
+position: Researcher
+webpage: https://www.doc.ic.ac.uk/~aloow/
+email: a.loow@imperial.ac.uk
+github: https://github.com/AndreasLoow
+alumnus: false
+projects:
+---
+
+Andreas did his PhD at Chalmers University of Technology, in Sweden, under the supervision of [Magnus Myreen](http://www.cse.chalmers.se/~myreen/). At Chalmers, Andreas worked on interactive theorem proving for software and hardware correctness. Specifically, he worked on building trustworthy computer systems, known as verified stacks, with full-system correctness theorems. Much of his work revolved around trustworthy hardware, for example in the form of the development and verification of the [Verilog synthesis tool Lutsig](https://dl.acm.org/doi/10.1145/3437992.3439916). Andreas defended his thesis, [Building Verified Hardware and Verified Stacks in HOL](https://www.doc.ic.ac.uk/~aloow/papers/thesis.pdf), in September 2021.

_people/maksimovic.md

 ---
 firstname: Petar
 lastname: Maksimović
-position: Research Fellow
+search_lastname: Maksimovic
+position: Researcher
 webpage: https://sites.google.com/site/petarmaksimovic1981/
 email: p.maksimovic@imperial.ac.uk
 github: PetarMax
+alumnus: true
 projects:
   - web
+  - moc
+  - sl
+  - gillian
 ---
 
+Petar Maksimović was a Research Fellow with the group and the Academic Program Manager for the [Research Institute on Verified Trustworthy Software Systems (VeTSS)](https://vetss.org.uk/) until his move to industry in 2022.
+
+Petar is also a Research Assistant Professor at the Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade.

_people/nantes.md

+---
+firstname: Daniele
+lastname: Nantes
+position: Researcher
+webpage: 
+email: d.nantes-sobrinho@imperial.ac.uk
+github:  
+alumnus: false
+projects:
+---
+
+[Daniele](https://mat.unb.br/dnantes/) is a tenured assistant professor at the Department of Mathematics, University of Brasília, and is currently in a long sabbatical leave. 
+
+Daniele's research focusses on equational reasoning and comparative expressiveness of models and languages with concurrency.  She was a researcher with the [Theoretical Computer Science Group (GTC-UnB)](https://www.mat.unb.br/ayala/TCgroup/index.html), and an external collaborator of the [VIDI project Unifying Correctness for Communicating Systems](https://www.jperez.nl/vidi). Her latest publications are [Formalising nominal C-unification generalised with protected variables](https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/formalising-nominal-cunification-generalised-with-protected-variables/0299ECF29C28FDD65AAE38E73BF28FE3), published in Mathematical Structures for Computer Science, and the conference papers [Nominal Equational Problems](https://link.springer.com/chapter/10.1007/978-3-030-71995-1_2), published in ETAPS’ Foundations of Software Science and Computation Structures (FOSSACS 2021) series, and [Non-deterministic Functions as Non-Deterministic Processes](https://drops.dagstuhl.de/opus/volltexte/2021/14259/), in Formal Structures for Computation and Deduction (FSCD 2021) series.

_people/naudziuniene.md

 ---
 firstname: Daiva
 lastname: Naudžiūnienė
+search_lastname: Naudziuniene
 position: PhD Student
-webpage: http://www.doc.ic.ac.uk/~dn911/
-email: d.naudziuniene11@imperial.ac.uk
-projects:
-  - web
-  - sl
+alumnus: true
 ---
+
+Daiva defended her PhD on [An Infrastructure for Tractable Verification of JavaScript Programs]({{site.baseurl}}{% link publications/Naudziuniene2018Infrastructure.html %}) in March 2018.
+
+Since 2017, Daiva has been working as a Research Scientist at Facebook as part of the engineering team led by Peter O’Hearn.

_people/ntzik.md

@@ -2,10 +2,10 @@
 firstname: Gian
 lastname: Ntzik
 position: PhD Student
-webpage: http://www.doc.ic.ac.uk/~gn408/
-email: gian.ntzik08@imperial.ac.uk
 github: anirothan
-projects:
-  - concurrency
+alumnus: true
 ---
 
+Gian was a PhD student and Post Doc with the group. Gian defended his thesis [Reasoning about POSIX File Systems]({{site.baseurl}}{% link publications/Ntzik2017Reasoning.html %}) 
+in February 2017 and is currently working for [Amadeus](http://www.amadeus.com/web/amadeus/en_GB-GB/Amadeus-Home/About-us/Our-company/1319477448520-Page-AMAD_DetailPpal) 
+in systems development and research.
\ No newline at end of file

_people/raad.md

@@ -2,10 +2,13 @@
 firstname: Azalea
 lastname: Raad
 position: PhD Student
-webpage: http://www.doc.ic.ac.uk/~azalea/
+webpage: http://www.soundandcomplete.org/
 email: azalea@imperial.ac.uk
-projects:
-  - concurrency
-  - sl
+alumnus: true
 ---
 
+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/). 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

+---
+firstname: Gabriela
+lastname: Sampaio
+position: PhD Student
+webpage: https://www.doc.ic.ac.uk/~gcs817/
+email:
+github:  
+alumnus: true
+projects:
+  - web
+  - moc
+---
+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  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,9 +3,11 @@ firstname: Julian
 lastname: Sutherland
 position: PhD Student
 webpage: http://www.doc.ic.ac.uk/~jhs110/
-email: jhs110@doc.ic.ac.uk
+email: 
+alumnus: true
 projects:
   - concurrency
   - sl
 ---
 
+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,10 +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
-projects:
-  - web
+webpage: https://twitter.com/IgnoredAmbience
+github: IgnoredAmbience
+alumnus: true
 ---
 
+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

@@ -5,7 +5,12 @@ position: PhD Student
 webpage: http://www.doc.ic.ac.uk/~sx14/
 email: shale.xiong14@imperial.ac.uk
 github: ShaleXIONG
+alumnus: true
 projects:
   - concurrency
+  - moc
 ---
 
+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/2016-07-26-advert.md

 ---
-title: One new postdoc position at Imperial College!
+title: One new postdoc position at Imperial College
 ---
 We are looking to recruit one postdoctoral researcher in the Program Specification and Verification Group at Imperial College London, to work on reasoning about concurrent programs. The position is suitable for either a theoretician, who would work on the foundations of concurrent reasoning, or a theoretician/practitioner, who would work on the verification and testing of file systems.
 
-<b> \*\*\* Deadline: 18th September \*\*\* </b>
+<b> \*\*\* Applications now closed \*\*\* </b>
 
-This position will have an initial duration of 2.5 years, with a certain level of flexibility with respect to the start date and possible extensions. It will be funded as part of the £5.6M EPSRC Programme Grant <a href="https://www.cl.cam.ac.uk/~pes20/rems/" target="_blank"> "REMS: Rigorous Engineering of Mainstream Systems"</a>, at the University of Cambridge, University of Edinburgh, and Imperial College London
+This position will have an initial duration of 2.5 years, with a certain level of flexibility with respect to the start date and possible extensions. It will be funded as part of the £5.6M EPSRC Programme Grant ["REMS: Rigorous Engineering of Mainstream Systems"](https://www.cl.cam.ac.uk/~pes20/rems/index.html), at the University of Cambridge, University of Edinburgh, and Imperial College London
 
 The Department of Computing at Imperial provides a vibrant and stimulating research environment in the heart of London, with leading research groups working on programming languages, verification, and testing. The quality of the Department has been consistently awarded the highest research and teaching rating. In the latest Research Excellence Framework assessment of 2014, the Department was ranked third (first in the Research Intensity table published by the Times Higher). In addition, at the last national assessment of teaching quality, the Department was rated as "Excellent" and came 2nd in The Complete University Guide, The Guardian, The Times and The Sunday Times national league tables by subject.
 
-The Program Specification and Verification Group is led by Professor Philippa Gardner, and its current focus is on reasoning about JavaScript and concurrency. The advertised position will target concurrency in particular (see http://psvg.doc.ic.ac.uk/research/concurrency.html). The breadth of the REMS project allows for flexibility in the profile of the candidate, who would work either on the foundations of concurrency reasoning or on the verification and testing of file systems.
+The Program Specification and Verification Group is led by Professor Philippa Gardner, and its current focus is on reasoning about JavaScript and concurrency. The advertised position will target [concurrency](/research/concurrency.html) in particular. The breadth of the REMS project allows for flexibility in the profile of the candidate, who would work either on the foundations of concurrency reasoning or on the verification and testing of file systems.
 
 <b> \*\*\* Foundations of concurrency reasoning \*\*\* </b> Recently, various program logics based on concurrent separation logic have been developed, by ourselves and others, with the aim of providing more modular abstract reasoning about concurrent programs. Our work at Imperial has tackled a range of problems, including data abstraction (Concurrent Abstract Predicates), abstract atomicity (the TaDA logic), fault-tolerance and progress, applying our reasoning to concurrent B-trees, skip lists from java.util.concurrent, graph algorithms, and the POSIX file system. The advertised position is suitable for someone interested in such foundational work on concurrency reasoning and, in particular, its relationship with respect to linearisability.
 

_posts/2016-09-01-newmember.md

+---
+title: Welcome to Andrea Cerone, new member of the group
+---
+We are very happy to welcome Andrea Cerone to the group. Andrea has joined us from the [IMDEA Software Institute](http://software.imdea.org/about.html), Madrid, Spain, 
+where he worked with Dr. Alexey Gotsman on Verification of Higher Order Concurrent Libraries and Foundations of Consistency Models for Distributed Databases. 
+
+Andrea is currently working on frameworks for specifying weak consistency models of geo-replicated databases and applications of transaction 
+chopping for various consistency models. Andrea did his Ph.D at Trinity College Dublin with Prof Matthew Hennessy, so he claims to be quite unfazed by the UK weather.
+
+You can find more about Andrea on [his webpage](https://www.doc.ic.ac.uk/~acerone/).
+
+

_posts/2016-09-15-daiva.md

+---
+title: Daiva Naudžiūnienė moving to Facebook
+---
+Congratulations to [Daiva Naudžiūnienė](https://www.doc.ic.ac.uk/~dn911/), who is off to work for Facebook in the new year. 
+
+Daiva is currently finishing her Ph.D. on reasoning about JavaScript with Philippa Gardner. 
+Over the summer, she spent three months as an intern working with the engineering team led by Peter O'Hearn at Facebook. 
+Daiva did very well and was invited to join the company full time next year, once she finishes her PhD.

_posts/2016-10-03-papers.md

+---
+title: Papers published by Azalea Raad
+---
+Azalea Raad has had two papers published in Programming Languages and System: Proceedings of the 14th Asian Symposium, [APLAS 2016](https://soict.hust.edu.vn/~aplas2016/).
+
+The papers are: [Verifying Concurrent Graph Algorithms](http://vtss.doc.ic.ac.uk/publications/Raad2016Verifying.html) (with Aquinas Hobor, Jules Villard and Philippa Gardner) and [DOM: Specification and Client Reasoning](http://vtss.doc.ic.ac.uk/publications/Raad2016DOM.html) (with José Fragoso Santos and Philippa Gardner).
+
+These and other group papers can be found on our [publications page](http://vtss.doc.ic.ac.uk/publications/).

_posts/2016-10-12-talk.md

+---
+title: Keynote talk at the IET SSCS Conference
+---
+Philippa Gardner was one of the keynote speakers at the 11th System Safety and Cyber Security Conference, (SSCS 2016) organised by the [IET](http://www.theiet.org/).
+
+Philippa’s talk, on Verified Trustworthy Software Systems was part of a panel discussion on the future of UK’s National Cyber Security Strategy. 
+The audience included academics, civil servants, safety and security engineers and leading technology companies such as Intel Security and QinetiQ. 
+Other sessions at the conference included topics on integrating safety and cyber security, legal and moral issues, implementing and adopting security approaches, system safety, software safety and transport.

_posts/2016-11-14-inferlab.md

+---
+title: Infer Lab at Imperial
+---
+
+The [Separation Logic]({{site.baseurl}}{% link teaching/separationlogic.md %}) course team ran a lab on [Infer](http://fbinfer.com/), 
+an automatic verification tool based on separation logic, developed at [Facebook](https://www.facebook.com/inferstaticanalyzer/) 
+where it is used every day to verify millions of lines of code.
+
+![Infer Lab](/images/images/Infer-lab-1.jpg)
+
+[Peter O’Hearn](http://www.pl-enthusiast.net/2015/09/15/facebooks-peter-ohearn-on-programming-languages/), 
+Engineering Manager and leader of the Infer team, came to talk about the use of Infer at Facebook. 
+[Jules Villard](https://www.doc.ic.ac.uk/~jvillar1/), Software Engineer at Facebook, gave a tutorial on bi-abduction, 
+based on the slides that he developed together with Daiva Naudžiūnienė whilst a Post-Doc at Imperial College London.
+
+The Imperial team then ran a lab on how to use [Infer](http://fbinfer.com/) to verify real world Android applications,
+using as examples PocketHub, Wikipedia Android app, DuckDuckGo and k-9 mail client. 
+During the tutorial, one of the students, Lorenzo Paoliani, ran Infer on ConnectBot, an SSH client for Android, 
+and found several null dereference bugs. He reported this on github and submitted a pull request for fixing that problem, 
+which has been accepted and now merged.
+
+For more details and slides, see the [Infer Lab 2016]({{site.baseurl}}{% link teaching/InferLab.md %}) page.
\ No newline at end of file

_posts/2016-11-23-dagstuhl.md

+---
+title: Talk at Dagstuhl Seminar
+---
+
+Andrea Cerone was invited to attend the seminar on [Concurrency with Weak Memory Models](http://www.dagstuhl.de/en/program/calendar/semhp/?semnr=16471) at Schloss Dagstuhl last week. 
+
+![Andrea Cerone at Dagstuhl with former colleague Giovanni Bernardi](/images/posts/Dagstuhl-Seminar-16.png)
+
+The seminar covered a wide range of topics, including fundamental results in the theory underlying weak memory models, 
+applications in the fields of hardware architectures, compiler optimisations and transactional systems, 
+as well as static analysis techniques for the analysis of programs. Andrea Cerone gave a talk on 'Analyzing Snapshot Isolation'.

_posts/2016-12-05-ECMA.md

+---
+title: JSExplain discussed at ECMAScript standards committee meeting
+redirect_from: /2016/12/05/EMAC.html
+---
+Thomas Wood attended the latest [ECMAScript standards committee TC39](https://github.com/tc39/) meeting this November in San Francisco.
+
+
+In previous meetings, we have presented a prototype of our JSExplain work to the committee and discussions with committee members at the latest meeting 
+furthered the design directions that JSExplain should take, to assist their needs with drafting revisions to the specification.
+    
+JSExplain is a reference interpreter derived from the JSCert project, 
+with a user interface designed to assist someone in their understanding of the workings of the ECMAScript language. 
+It is hoped that in the long run, the language the JSExplain specification is written in will closely match the English language of the specification. 
+Using it as an aid to drafting the specification will be  the natural next step, 
+with the added advantage that the new features being proposed can be tested and experimented with interactively during their development.
+
+It is envisaged that the JSExplain specification will be extractable for use in theorem provers to prove theories about the language, for example, 
+the soundness of the invariants [specified for Object internal methods](https://tc39.github.io/ecma262/2017/#sec-invariants-of-the-essential-internal-methods).
+    
+A [preliminary prototype version](https://jscert.github.io/jsexplain/branch/master/driver.html) of JSExplain is available, along with the [source code](https://github.com/jscert/jsexplain).
+
+JSExplain is a collaboration with [Charguéraud](http://chargueraud.org/) and [Schmitt](http://people.rennes.inria.fr/Alan.Schmitt/) of [INRIA](http://www.inria.fr/).
+
+Thomas has also agreed to assist with the [Regular Expression Lookbehind Assertions Proposal](https://github.com/littledan/es-regexp-lookbehind) targeted for the ES2017 specification.

_posts/2016-12-15-Dolby.md

+---
+title: Visit from Julian Dolby, IBM
+---
+[Julian Dolby](http://researcher.watson.ibm.com/researcher/view.php?person=us-dolby), a researcher at IBM's 
+[Thomas J. Watson Research Center](http://www.research.ibm.com/labs/watson/index.shtml)
+in New York visited the VTSS group for a week in December.
+
+Julian’s research focuses on static program analysis, 
+software testing and the semantic web and during his visit, Julian worked with José Fragoso and Petar Maksimovic 
+in a [symbolic analysis for JavaScript]({{site.baseurl}}{% link research/javascript.md %}) 
+based on JSIL and Rosette with the end goal of having a bug-finding tool for JavaScript.
+
+[ROSETTE](https://github.com/juliandolby/rosette) is a solver-aided programming language 
+that extends Racket with language constructs for program synthesis, verification, and more.