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

_posts/2022-04-26-daniele.md

+---
+title: Welcome to Daniele Nantes, new researcher with the group
+---
+
+A very warm welcome to Daniele Nantes Sobrinho, who has joined the group as a research assistant. Daniele is a tenured assistant professor at the [Department of Mathematics, University of Brasília](https://euro-math-soc.eu/affiliation/department-mathematics-university-brasilia), and is currently in a long sabbatical leave.
+
+Daniele’s research focusses on equational reasoning and comparative expressiveness of models and languages with concurrency. You can see her [latest publications here](http://vtss.doc.ic.ac.uk/people/nantes.html).

_posts/2022-05-15-floc22.md

+---
+title: Daniele Nantes, papers accepted at FSCD, FLoC 2022
+---
+
+Daniele Nantes has had two papers accepted at [FSCD, the 7th International Conference on Formal Structures for Computation and Deduction](https://www.cs.tau.ac.il/~nachumd/FSCD/), part of the [8th Federated Logic Conference (FLoC 2022)](https://www.floc2022.org/)
+
+Daniele will present the papers, [Nominal Anti-Unification with Atom Variables](https://drops.dagstuhl.de/opus/volltexte/2022/16288/), with Schmidt-Schauss and [A Certified Algorithm for AC Unification](https://drops.dagstuhl.de/opus/volltexte/2022/16289/), with Ayala-Rincón, Férnandez, and Ferreira da Silva, at this year’s conference, which will be held in Haifa, Israel.

_posts/2022-06-02-julian.md

+---
+title: Many congratulations to Dr Julian Sutherland
+---
+
+We are very, very happy to announce that Julian Sutherland, a long standing member of the group, has very successfully defended his PhD thesis today. 
+
+Many congratulations to Julian, and many thanks to [Derek Dreyer](https://www.mpg.de/18617632/software-systems-dreyer), [Joseph Tassarotti](http://www.cs.bc.edu/~tassarot/) and [Sophia Drossopoulou](https://wp.doc.ic.ac.uk/sd/), who acted as the examiners.
+
+Julian’s thesis, Compositional termination verification for fine-grained concurrency, focuses on TaDA Live, a separation logic for proving liveness properties of concurrent programs.  
+
+Liveness properties are concerned with showing that a program eventually reaches some desired state, in contrast to safety properties, which involve showing that a program never reaches a "bad/unsafe" state. Research work on proving liveness properties remains challenging and TaDA Live represents a substantial innovation, as it can handle reasoning about both non-blocking and blocking examples. 
+
+TaDA Live can reason about the termination of clients which use abstract atomic operations that have blocking behaviour arising from busy-waiting patterns without breaking their abstraction boundaries, and the correctness of the implementations of the operations with respect to their abstract specifications. The thesis also introduces a novel semantic model using layered subjective obligations to express liveness invariants, and a proof system that is sound with respect to the model.
+
+Julian is currently a Formal Verification Engineer at [Nethermind](https://nethermind.io/), a blockchain company working on Ethereum.

_posts/2022-06-13-pldi.md

+---
+title: Technical talk at Programming Language Mentoring Workshop (PLMW)
+---
+
+Philippa Gardner gave an technical talk at this year’s [Programming Language Mentoring Workshop (PLMW](https://pldi22.sigplan.org/track/PLMW-PLDI-2022#event-overview)), part of [PLDI 2022](https://pldi22.sigplan.org/). 
+
+The workshop is aimed at students interested in developing a career in programming languages and includes technical talks, discussions and mentoring sessions. It is co-located with the conference on [Programming Language Design and Implementation (PLDI)](https://pldi22.sigplan.org/).
+
+After two years on-line, PLDI 2022 was held in person this year, which allowed for a [live rendition of the PLDI song by a bunch of familiar faces!](https://www.youtube.com/watch?v=N9V-w4vwZeg). 

_posts/2022-06-14-types21.md

+---
+title: Daniele Nantes, paper published, TYPES
+---
+
+Daniele’s paper [Types and Terms Translated: Unrestricted Resources in Encoding Functions as Processes](https://drops.dagstuhl.de/opus/volltexte/2022/16780/pdf/LIPIcs-TYPES-2021-11.pdf) has been published as part of the proceedings of the [27th International Conference on Types for Proofs and Programs,(TYPES)](https://types21.liacs.nl/), organised by the Leiden Institute of Advanced Computer Science, in the Netherlands.
+
+The [TYPES meetings](https://sites.google.com/view/thetypesconferences) are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalized and computer assisted reasoning and computer programming.

_posts/2022-06-30-vistas.md

+---
+title: Vistas in Verified Software, workshop at the Isaac Newton Institute, talks live-streamed
+---
+
+Philippa Gardner is one of the organisers, together with Azadeh Farzan, Natarajan Shankar and Moshe Vardi, of the [Vistas in Verified Software workshop](https://www.newton.ac.uk/event/vs2w01/) which will take place at the Isaac Newton Institute (INI) on 4-8 July 2022.
+
+The Vistas in Verified Software workshop features invited talks from distinguished researchers spanning machine learning, distributed systems, concurrency, networking, cyber-physical systems, programming languages, and program analysis. 
+
+Talks will be live streamed in the [INI live stream link](https://www.newton.ac.uk/news/watch-live/) and some will also be recorded and made available afterwards at the [INI You Tube channel.](https://www.youtube.com/playlist?list=PL9-ncTy2ag0FMw3BDhlKUGc_RGU1dok6M)
+
+The workshop is part of a six week  programme on [Verified software](https://www.newton.ac.uk/event/vso2/), aimiing to bring together researchers from across the world for a wide range of talks and discussions on the theoretical and practical challenges in formal verification and certification of software systems. The gathering will allow participants to take stock of the first fifteen years of [Tony Hoare’s Verified Software Challenge](http://vstte.inf.ethz.ch/pdfs/vstte-hoare-misra.pdf) and to formulate a concrete roadmap for international cooperation for the next fifteen years.

_posts/2022-07-26-concurrency.md

+---
+title: Concurrency meeting at the Isaac Newton Institute in Cambridge, August 2022
+---
+
+[John Wickerson](https://johnwickerson.github.io), [Azalea Raad]( https://www.soundandcomplete.org), Philippa Gardner and [Andreas Lööw]( https://www.doc.ic.ac.uk/~aloow/) are the organisers of this year’s [UK Concurrency Workshop](https://johnwickerson.github.io/cw2022.html). which will be held on 11-12 August 2022 at the [Isaac Newton Institute (INI)](https://www.newton.ac.uk) in Cambridge.
+
+This will be the final event in the [Verified Software programme](https://www.newton.ac.uk/event/vso2/) that has been running at the institute this summer. 
+
+The two-day meeting aims to bring together researchers from the UK and elsewhere, who are working on the theory of concurrency and related areas. The talks will cover a wide range of research at various stages of development (work-in-progress, mature projects, and anywhere in-between) are welcome. The workshop is free to attend in person and virtually. 

_posts/2022-08-01-asl22.md

+---
+title: Philippa Gardner, Keynote at Advances in Separation Logics (ASL 2022)
+---
+
+Philippa was one of the two keynote speakers at this year’s Advances in [Separation Logics (ASL 2022) workshop](https://asl-workshop.github.io/asl22/), which was held online. 
+
+Philippa’s talk was on her latest work on [Exact Separation Logic (ESL)](https://vtss.doc.ic.ac.uk/publications/Maksimovic2022Exact.html) for reasoning about heap-manipulating sequential programs, a logic which provides fully verified function specifications compatible with true bug finding.
+
+ASL 2022 aims to bring together researchers and practitioners interested on improving the state of the art of automated deduction methods for Separation Logic and is affiliated to [IJCAR 2022](https://ijcar.org/), part of [FLOC 2022, the 8th Federated Logic Conference.](https://www.floc2022.org/)

_posts/2022-08-04-wil22.md

+---
+title: Daniele Nantes, co-chair of this year’s Women in Logic (WiL) workshop
+---
+Daniele is one of the co-chairs of this year’s [Women in Logic 2022 (WiL)](https://sites.google.com/g.uporto.pt/wil2022/home/pc), a co located event part of the [8th Federated Logic Conference (FLoC 2022)](https://www.floc2022.org/) to be held in Haifa, Israel, this summer 2022. 
+
+She is also one of the organisers of the conference [Women’s@FLOC dinner] (https://www.floc2022.org/womens-at-floc-microsoft)
+
+The [Women in Logic workshop (WiL)](https://www.womeninlogic.org/) promotes research done by women in logic in computer science, working to increase their visibility and representation in the community.

_posts/2022-08-31-kashish.md

+---
+title: Kashish Raimalani, UROP with the group
+---
+
+Thank you and goodbye to Kashish Raimalani, from the University of Manchester, who has spent two months working with the group. 
+
+Kashish joined us as part of this year’s [Undergraduate Research Opportunities Programme (UROP)](https://www.imperial.ac.uk/urop) where undergraduate students spend time over the summer with a research group. 
+
+During her time with us, Kashish worked on first-order unification/matching and extracted a pseudocode implementation of the algorithm for building matching plans that is currently implemented in [Gillian.](https://github.com/GillianPlatform/Gillian) 
+
+Kashish also built examples that motivated a more precise definition of matching plans and participated in the theoretical design of a match-and-consume algorithm implemented in Haskell, for a fragment of the language of expressions of separation logic. 
+
+We are very grateful to Kashish for all her hard work and wish her all the best as she returns to Manchester to continue her studies.

_posts/2022-10-10-karmios.md

+---
+title: Nat Karmios, new research engineer in the group
+---
+
+We are very happy to welcome Nat Karmios, who has joined the group as Research Engineer. 
+
+Nat has several years of industry experience, has recently completed an MEng in Computing 
+at Imperial and will work on improving Gillian's accessibility through the development 
+of a visual debugger for symbolic execution and verification.

_posts/2022-12-07-lab.md

+---
+title: Gillian lab, Scalable Software Verification course
+---
+
+Students on the 4th year, MEng and MSc course [Scalable Software Verification](https://vtss.doc.ic.ac.uk/teaching/separationlogic.html) attended a lab session on [Gillian](https://github.com/GillianPlatform), a compositional symbolic analysis tool instantiated to JavaScript and C.
+
+![Gillian Lab](/images/posts/Gillian_Lab.jpg){: width="400"}
+
+During the lab, the students tried out the new debugger interface recently developed by Nat Karmios and tested a range of examples, applying the knowledge gained during the course to real live symbolic testing. Feedback from the lab was very positive, and the plan is to run the lab again next year.

contact.md

@@ -8,17 +8,17 @@ redirect_from: /contact.html
 
 <iframe src="https://www.google.com/maps/embed?pb=!1m18!1m12!1m3!1d2483.779882328909!2d-0.18118674906856128!3d51.49890671904571!2m3!1f0!2f0!3f0!3m2!1i1024!2i768!4f13.1!3m3!1m2!1s0x4876055c7df7c537%3A0x2541470e75df5fe0!2sHuxley+Building!5e0!3m2!1sen!2suk!4v1490695192578" width="500" height="500"  frameborder="0" allowfullscreen style="float:right;border:0">Google Map</iframe>
 
-### Teresa Carbajo Garcia
-<h6 class="text-muted">Administrative Program Manager</h6>
+### Teresa Ng
+<h6 class="text-muted">Program Manager</h6>
 
 
 ##### Email
 
-<a href="mailto:t.carbajo-garcia@imperial.ac.uk" style="color:black">t.carbajo-garcia@imperial.ac.uk</a>
+<a href="mailto:t.ng@imperial.ac.uk" style="color:black">t.ng@imperial.ac.uk</a>
 
 ##### Phone
 
-+44 (0)20 7594 43140
++44 (0) 20 7594 8300
 
 ##### Address