Apr 26, 2022
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, and is currently in a long sabbatical leave.
Apr 4, 2022
Sacha Ayoun and Petar Maksimovic gave a talk on Gillian-Rust: Unified Symbolic Analysis for Rust at the Second Rust Verification Workshop (RW2022), which was held in Munich, Germany, co-located with ETAPS 2022
Mar 29, 2022
Many congratulations to Gabriela Sampaio, who defended her PhD thesis, A Trusted Infrastructure for Symbolic Analysis of Event based Web APIS very succesfully today.
Nov 5, 2021
Nov 1, 2021
Welcome back to Sacha who has returned from a three-months internship with the CodeGuru team at Amazon Web Services.
Oct 3, 2021
A very warm welcome to Andreas Lööw, who has just started with us as a Post-Doctoral researcher.
Sep 3, 2021
We are very happy to welcome Caroline Cronjager, a visiting student from Ruhr University Bochum, Germany.
Aug 14, 2021
Philippa Gardner has been announced as one of the recipients of the Spring 2021 Amazon Research Awards (ARA).
Jul 2, 2021
Many congratulations to Emanuele D’Osualdo, Azadeh Farzan, Philippa Gardner and Julian Sutherland, whose paper “TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs” has been accepted for publication at the ACM Transactions on Programming Languages and Systems (TOPLAS) journal.
Jun 16, 2021
Congratulations to friends and colleagues Conrad Watt, Xiaojia Rao, Jean Pichon-Pharabod, Martin Bodin and Philippa Gardner, whose paper “Two mechanisations of WebAssembly 1.0” has been accepted at the 24th International Symposium of Formal Methods (FM21).
May 31, 2021
Congratulations to Petar, Jose, Sacha and Philippa, whose paper and artifact have been accepted to CAV 2021, the 33rd International Conference on Computer-Aided Verification.
May 12, 2021
Welcome (again) to Gabriela who has returned from her second industry internship, this time a three-months placement with the Static Analysis Tools team at Facebook London.
May 4, 2021
Another year, another PLDI conference, another excellent PLDI song and video: “Pure Implementation”, displaying the musical talents of many friends and colleagues.
Apr 15, 2021
Philippa Gardner gave a talk on Gillian: a Multi-language Platform for Compositional Symbolic Analysis at the College de France, as part of their Program logic seminars.
Apr 6, 2021
Philippa is one of the organisers of two upcoming workshops on Verification at the Isaac Newton Institute for Mathematical Sciences, in advance of their scientific programme on Verified Software, which had to be postponed last summer.
Jan 14, 2021
Jan 12, 2021
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.
Dec 1, 2020
The fourth Facebook Testing and Verification Symposium (TAV) will take place this week, with an interesting programme of speakers including our own Alastair Donaldson and Philippa Gardner.
Nov 4, 2020
Philippa will be one of the speakers at this year’s Code Mesh, a two-day conference on functional programming languages and alternative tech.
Oct 1, 2020
A very warm welcome to Xiaojia Rao who has just joined the group as a PhD student.
Oct 1, 2020
Goodbye and our best wishes to Martin Bodin who is leaving the group to join the Inria Grenoble-Rhône-Alpes Research Centre, France, as a CRCN (chargé de recherche de classe normale) in the Sound Programming of Adaptive Dependable Embedded Systems (Spades) group.
Sep 27, 2020
Philippa was one of 53 engineers in the UK to be elected to the Fellowship of the Royal Academy of Engineering this year.
Sep 3, 2020
The talk by Emanuele D’Osualdo and Felix Stutz on their paper “Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions”, presented at CONCUR 2020, is now available online and can be seen on the link here or below.
Sep 1, 2020
Goodbye and our best wishes to Emanuele D’Osualdo, who is joining Derek Dreyer’s group at the Max Planck Institute for Software Systems (MPI-SWS) in Saarbrücken, Germany in September.
Aug 31, 2020
Congratulations to Emanuele D’Osualdo and Felix Stutz, whose paper, Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions, has been accepted at this year’s CONCUR.
Jun 19, 2020
The talk by Petar Maksimovic on Gillian: a Multi-language Platform for Program Correctness and Incorrectness, presented at PLDI 2020, is now available on the PLDI YouTube channel, and can be seen on the link here or below.
Jun 16, 2020
The REMS+DeepSpec workshop organized jointly by the EPSRC project REMS: Rigorous Engineering for Mainstream Systems (Cambridge, Imperial, and Edinburgh, UK) and the NSF Expedition in Computing “The Science of Deep Specification” (US) was held on Mon 15 - Tue 16 Jun 2020.
Jun 16, 2020
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 directly as soon as possible.
May 19, 2020
This year’s PLDI has moved online and the organisers have just posted a song to remind attendees that virtually or not, this is still PLDI.
May 11, 2020
Congratulations to Jose Fragoso, Petar Maksimovic, Sacha Ayoun and Philippa Gardner, whose paper, Gillian, Part I: A Multi-language Platform for Symbolic Execution, has been accepted at this year’s PLDI.
Apr 27, 2020
Two papers by members of the group have been accepted at the 34th European Conference on Object-Oriented Programming, ECOOP 2020.
Feb 20, 2020
Many congratulations to Shale Xiong, who very successfully defended his PhD thesis, Parametric Operational Semantics for Consistency Models today.
Jan 22, 2020
Philippa was one of the speakers at the Interactive Knowledge Shares session of this year’s HASE, the Workshop on High Assurance Systems Engineering
Nov 11, 2019
Philippa Gardner is one of the organisers of the six week programme Verified Software at the Isaac Newton Institute, Cambridge.
Oct 30, 2019
The third annual Facebook testing and verification symposium will be held on 20-21 November in London.
Oct 28, 2019
Philippa Gardner, Emanuele D’Osualdo and Julian Sutherland attended the first edition of the Iris workshop.
Oct 1, 2019
Julian Sutherland has just returned from a three months internship with the Facebook’s Infer team.
Sep 26, 2019
Philippa Gardner was one of the organisers of the `Verified Software’ workshop, held at the Isaac Newton Institute for Mathematical Sciences, (INI), Cambridge on 24th-25th September 2019.
Aug 15, 2019
Aug 9, 2019
Jul 26, 2019
Emanuele D’Osualdo and Shale Xiong both gave talks at this year’s Surrey Concurrency Workshop and S-REPLS.
Jun 3, 2019
Philippa Gardner and Emanuele D’Osualdo are part of the local organising team for the 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) which is taking place in London this week.
May 31, 2019
Our very best wishes to Andrea Cerone, who after three years with the group is leaving to take up a position as a software engineer for Footballradar.
Effective Verification Workshop at the Lorentz centre, talks by Philippa Gardner and Emanuele D’Osualdo
May 13, 2019
Philippa Gardner and Emanuele D’Osualdo gave invited talks as this May’s Lorentz centre workshop: Effective Verification: Static Analysis Meets Program Logics in Leiden, The Netherlands.
May 1, 2019
Martin Bodin gave a talk “A Trustworthy Mechanized Formalization of R“ at the Formal Methods for Statistical Software (FMfSS 2019) workshop, to present his work on big-step operational semantics for R. The abstract for the talk is below.
Apr 1, 2019
Congratulations to Petar Maksimović and Philippa Gardner, whose paper with Conrad Watt and Neel Krishnaswami (University of Cambridge) has been accepted at this year’s European Conference on Object-Oriented Programming (ECOOP ‘19)
Nov 10, 2018
Congratulations to José Fragoso Santos, Philippa Gardner, Petar Maksimović, Martin Bodin and Gaby Sampaio, whose papers were accepted at this year’s ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019).
Nov 7, 2018
Oct 15, 2018
We are very happy to welcome Sacha Ayoun, who has joined the group as a PhD student.
Sep 3, 2018
Philippa Gardner, Established Career Fellowship, VeTSpec, Verified Trustworthy Software Specification
Sep 2, 2018
Philippa Gardner has been awarded an Established Career Fellowship by the UK Research and Innovation (UKRI).
Sep 1, 2018
Many congratulations to Emanuele, whose project “Verification through Security and Progress Abstractions” (VeSPA) was awarded a two year Marie-Curie Individual Fellowship, hosted at Imperial College.
Jul 16, 2018
Felix Stutz gave a talk on Monday on Automated Verification of Security Protocols. He presented the latest work on the project he is doing with Emanuele D’Osualdo and which will inform his Master Thesis.
Jun 13, 2018
Apr 23, 2018
We are very pleased to welcome Felix Stutz, an MSc student at the International Max Planck Research School for Computer Science, who is due to spend five months with the group, working with Emanuele D’Osualdo on Ideal completions for Verification of Cryptographic Protocols.
Apr 18, 2018
A paper co-authored by current and former researchers of the group has just been publised. A second paper, also collaborative work with current and former researchers has also just been accepted to ECOOP 18.
Mar 19, 2018
Mar 1, 2018
Feb 14, 2018
Dr Justin Hsu of University College of London visited the group this week to give a talk about probabilistic coupling: “From Couplings to Probabilistic Relational Program Logics”.
Jan 31, 2018
Dr Chung-Kil Hur of the Seoul National University came to visit the group and to talk about a promising semantics for relaxed-memory concurrency, published at POPL’17 and joint work with Jeehoon Kang from Seoul National University, and Ori Lahav, Viktor Vafeiadis and Derek Dreyer from MPI-SWS.
Jan 29, 2018
We are very happy to welcome Theotime Grohens who will be spending three months with the group at the beginning of the year.
Jan 15, 2018
Jan 12, 2018
Jan 6, 2018
Philippa Gardner is currently looking for a PhD student, start date in October 2018, to join the Verified Trustworthy Software Specification Group,
Dec 7, 2017
Nov 24, 2017
We are very pleased to have welcomed Siddharth Krishna, from the Courant Institute of Mathematical Sciences, NYU, who visited the group this week to talk about his work on the verification of concurrent data structures.
Nov 15, 2017
Oct 2, 2017
We are really happy to welcome Gabriela Sampaio, who has joined the group as a PhD student.
Sep 26, 2017
José Fragoso Santos, Philippa Gardner, Petar Maksimović, Daiva Naudžiūnienė and Thomas Wood, have had a paper accepted at this year’s ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).
Sep 22, 2017
Almost a hundred participants attended this year’s FMATS, held on 21-22 September 2017 at Microsoft Research Cambridge.
Philippa Gardner, Keynote talk at Reliably Secure Software Systems (RS3) meeting, Darmstadt, Germany.
Sep 6, 2017
Invited paper at the 26th International Conference on Automated Reasoning, (CADE), Gothenburg, Sweden.
Aug 12, 2017
Philippa Gardner was one of the invited speakers at the this year’s CADE conference, held in Gothenburg, Sweden, on 6-11 August 2017.
Jul 7, 2017
Jul 3, 2017
We are delighted to welcome Thomas Pointon, Samuel Ogunmola and Ashley Davies-Lyons who will be working with the group this summer as part of Imperial’s Undergraduate Research Opportunities Programme (UROP).
Jun 16, 2017
Andrea Cerone has had a paper accepted at this year’s International Conference on Concurrency Theory, (Concur 2017) which will be held in Berlin, Germany in September.
Jun 13, 2017
Emanuele D’Osualdo has had a paper accepted at this year’s Computer Security Foundations Symposium (CSF).
May 25, 2017
May 25, 2017
Many congratulations to Dr Azalea Raad, who has accepted a position as a Postdoctoral Fellow at the Max Planck Institute for Software Systems in Kaiserslautern, Germany, starting in July.
May 17, 2017
Best wishes to Dr Gian Ntzik, who will move to Amadeus at the end of May to work in systems development and research.
May 9, 2017
May 8, 2017
Philippa Gardner, Azalea Raad, Andrea Cerone and Emanuele D’Osualdo will be attending the Aarhus Concurrency Workshop on Concurrency Theory and related topics at the end of month.
Philippa Gardner, talk at the open Workshop on Consistency in Distributed Storage Systems, LIP6, Paris
May 3, 2017
May 1, 2017
We were delighted to host Dr Azadeh Farzan of the University of Toronto, who visited the group for two weeks to discuss her work, which involves Software Verification, Programming Languages, Formal Methods, and Security, all with an emphasis on concurrency-related issues.
Apr 28, 2017
Philippa Gardner was one of the keynote speakers at the 7th IPM International Conference on Fundamentals of Software Engineering (FSEN 2017) held in Tehran, Iran.
Apr 24, 2017
A very warm welcome to Emanuele D’Osualdo, who joined the group this week.
Philippa Gardner, invited speaker at Colloquium d'Informatique, Université Pierre et Marie Curie, Paris
Mar 28, 2017
Philippa Gardner was the invited speaker at the March 17 edition of the Colloquium d’Informatique de L’UPMC Sorbonne Universités.
Feb 20, 2017
Feb 14, 2017
Philippa Gardner attended the official opening by the Queen of the National Cyber Security Centre’s new headquarters in London. The NCSC, part of GCHQ, aims to make their work on cyber security more open; it will publish research, organise events and will provide advice on cyber security to businesses and members of the public.
Feb 11, 2017
Over sixty people attended the Introduction to Verification and Testing workshop, held this week at Imperial College London. The INVEST workshop, organised by Alastair Donaldson, Christian Cadar and Philippa Gardner gives young researchers and final year students with an interest in research the chance to take a closer look at the fields of software verification and testing.
Feb 10, 2017
Congratulations to Azalea Raad who very successfully defended her PhD thesis, Abstraction, Refinement and Concurrent Reasoning on Friday 10 February.
Feb 6, 2017
Two papers from the concurrency project team have been accepted at 26th European Symposium on Programming (ESOP 2017), which will take place this April in Uppsala, Sweden. The first paper, Abstract Specifications for Concurrent Maps, present the importance of abstract atomicity for reasoning fine-grained concurrent modules. The second paper, Caper: Automatic Verification for Fine-grained Concurrency, presents a prototype tool for automated reasoning about concurrent modules.
Feb 1, 2017
Jan 20, 2017
Jan 13, 2017
Congratulations to Pedro da Rocha Pinto who defended his PhD thesis, Reasoning with Time and Data Abstractions at his viva on Friday 13th January 2017.
Dec 15, 2016
Dec 5, 2016
Thomas Wood attended the latest ECMAScript standards committee TC39 meeting this November in San Francisco.
Nov 23, 2016
Andrea Cerone was invited to attend the seminar on Concurrency with Weak Memory Models at Schloss Dagstuhl last week.
Nov 14, 2016
Oct 12, 2016
Philippa Gardner was one of the keynote speakers at the 11th System Safety and Cyber Security Conference, (SSCS 2016) organised by the IET.
Oct 3, 2016
Azalea Raad has had two papers published in Programming Languages and System: Proceedings of the 14th Asian Symposium, APLAS 2016.
Sep 15, 2016
Congratulations to Daiva Naudžiūnienė, who is off to work for Facebook in the new year.
Sep 1, 2016
We are very happy to welcome Andrea Cerone to the group. Andrea has joined us from the IMDEA Software Institute, Madrid, Spain, where he worked with Dr. Alexey Gotsman on Verification of Higher Order Concurrent Libraries and Foundations of Consistency Models for Distributed Databases.
Jul 26, 2016
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.