_posts/2019-11-11- ini_workshop.md

+---
+title: Six week programme Verified Software at the Isaac Newton Institute, Cambridge
+---
+
+Philippa Gardner is one of the organisers of the [six week programme Verified 
+Software at the Isaac Newton Institute]( https://www.newton.ac.uk/event/vso
+), Cambridge. 
+
+The Verified Software programme includes two workshops, one on 
+the [Theory and Applications of Verified Software, From Theory to Practice](https://www.newton.ac.uk/event/vsow01) 
+and a second one on [Verification Tools and Experiments]( https://www.newton.ac.uk/event/vsow02). 
+These will be supplemented with smaller workshops and working groups devoted to specialized topics and industrial applications. 
+
+The aim of the programme is to bring together a diverse mix of 
+researchers to take stock of the first fifteen years of [Tony Hoare’s Verified 
+Software Challenge](https://www.researchgate.net/publication/221160548_Verified_Software_Theories_Tools_Experiments_Vision_of_a_Grand_Challenge_Project) 
+and formulate a concrete roadmap for international cooperation for the next fifteen years.
+
+Participation is by invitation only, but members of Cambridge University 
+are welcome to sign in as a non-registered attendee on the day(s) and attend 
+the lecture(s) and there are also [options to participate remotely}(https://www.newton.ac.uk/events/how-to-participate), 
+as most of the seminars at INI are streamed live and are made available for download as a webseminar shortly after the event.
\ No newline at end of file

_posts/2020-01-22-hase.md

+---
+title: Talk on Gillian, Workshop on High Assurance Systems Engineering, POPL2020
+---
+
+Philippa was one of the speakers at the [Interactive Knowledge 
+Shares session](https://popl20.sigplan.org/details/hase-2020-papers/2/Interactive-Knowledge-Shares) 
+of this year’s [HASE, the Workshop on High Assurance Systems Engineering]( https://popl20.sigplan.org/home/hase-2020)
+
+HASE, part of [POPL](https://popl20.sigplan.org), aims to bring about new collaborations 
+and launch shared initiatives to provide high levels of assurance about the correct operation and security properties 
+of production systems (software and hardware).
+
+Philippa presented Gillian, a language independent framework supporting 
+compositional symbolic analysis. Gillian supports three flavours of analysis: 
+whole-program symbolic testing, full verification, and bi-abduction. It comes with 
+fully parametric meta-theoretical results and a modular implementation, designed 
+to minimise the instantiation effort required of the user.
\ No newline at end of file

_posts/2020-02-20-shale.md

+---
+title: Congratulations to Dr Shale Xiong
+---
+
+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)
+who acted as the examiners.
+
+Shale's thesis develops a novel operational semantics for distributed key-value stores.
+This model combines the evolution of a global multi-versioning view and the client-local partial views and the
+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)

_posts/2020-04-27-ecoop.md

+---
+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 
+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, 
+JavaScript Promises, and the JavaScript async/await APIs, all underpinned by a simple 
+Core Event Semantics that is sufficiently expressive to describe the event models 
+underlying all these APIs. The implementations follow the API respective standards 
+line-by-line and have been thoroughly tested. An associated artifact was also 
+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 an interleaving operational semantics for 
+describing the client-observable behaviour of atomic transactions 
+on distributed key-value stores.
+
+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.
+
+Congratulations to all!
\ No newline at end of file

_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

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