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

accessibility/accessibility.md

+---
+title: Accessibility
+layout: page
+permalink: /accessibility/
+redirect_from: /accessibility.html
+---
+
+
+This statement applies to content published on [https://vtss.doc.ic.ac.uk](https://vtss.doc.ic.ac.uk).
+
+We want as many people as possible to be able to use this website. For example, that means you should be able to: 
+ 
+- Navigate most of the website using just a keyboard 
+- Listen to most of the website using a screen reader (including JAWS, NVDA and VoiceOver). 
+- Resize to the size of your window, and display a readable text size whichever device you are using 
+- Zoom in up to 175% without the text spilling off the screen 
+ 
+[AbilityNet](https://mcmw.abilitynet.org.uk/) also has advice on making your device easier to use if you have a disability. 
+ 
+## How accessible the website is 
+ 
+Parts of this website are not fully accessible. For example: 
+- some pages have poor colour contrast 
+- some heading elements are not consistent 
+- some images do not have good alternative text 
+- some buttons are not correctly identified 
+- many older documents in PDF format are not fully accessible 
+- some tables do not have row headers 
+- What we do about known issues 
+
+We work to achieve and maintain [WCAG 2.1 AA standards](https://www.w3.org/TR/WCAG21/), but it is not always possible for all our content to be accessible. Where content is not accessible, we will state a reason, warn users and offer alternatives. 
+
+## Technical information about this website’s accessibility 
+
+As part of Imperial College London, we are committed to making its website accessible in accordance with the Public Sector Bodies (Websites and Mobile Applications) (No. 2) Accessibility Regulations 2018. 
+
+This website is partially compliant with the [Web Content Accessibility Guidelines version 2.1 AA standard](https://www.w3.org/TR/WCAG21/), due to the known issues listed below. 
+
+## Non accessible content 
+
+We are currently carrying out accessibility testing on different aspects of the website. Once this is complete, we will update this section with any areas of the website which do not meet accessibility standards. 
+
+The content that is not accessible is outlined with details of: 
+- where it fails the success criteria 
+- planned dates for when issues will be fixed
+ 
+[View our current list of non accessible content]({{ '/accessibility/non-accessible-list/' | relative_url }})
+
+Some documents and content are [exempt from the regulations](https://www.legislation.gov.uk/uksi/2018/952/regulation/4/made) (such as live video content and PDFs or other documents published before 23 September 2018 if they’re not essential to providing our services), so we do not currently have any plans to make them accessible. But if you need to access information in one of these document types, you can contact us and ask for an alternative format.
+
+## Reporting accessibility issues
+
+If you need information on this website in a different format like accessible PDF, large print, easy read, audio recording or braille or if you find any accessibility issues not listed on this page then please contact Teresa Carbajo Garcia at [t.carbajo-garcia@imperial.ac.uk](mailto:t.carbajo-garcia@imperial.ac.uk) or Petar Maksimovic at [p.maksimovic@imperial.ac.uk](mailto:p.maksimovic@imperial.ac.uk). We’ll consider your request and get back to you within seven days. 
+
+ 
+## Enforcement procedure 
+
+The Equality and Human Rights Commission (EHRC) is responsible for enforcing the Public Sector Bodies (Websites and Mobile Applications) (No. 2) Accessibility Regulations 2018 (the ‘accessibility regulations’). If you’re not happy with how we respond to your complaint, [contact the Equality Advisory and Support Service (EASS)](https://www.equalityadvisoryservice.com/). 
+
+ 
+## How we test this website 
+
+This website is currently being tested for accessibility compliance, and these tests are being carried out internally through an external software testing. 
+
+ 
+## Last updated 
+ 
+This statement was prepared on 20 October 2020. It was last updated on 20 October 2020. 

accessibility/non_accessible_list.md

+---
+title: List of non-accessible content
+layout: page
+permalink: /accessibility/non-accessible-list/
+---
+
+Parts of this website are not fully accessible. For example: 
+- some pages have poor colour contrast 
+- some heading elements are not consistent 
+- some images do not have good alternative text 
+- some buttons are not correctly identified 
+- many older documents in PDF format are not fully accessible 
+- some tables do not have row headers 
+- What we do about known issues 
\ No newline at end of file

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