News
Goodbye to Martin Bodin
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.
Video talk on Decidable Inductive Invariants at CONCUR 2020
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.
Goodbye to Emanuele D’Osualdo
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.
Paper accepted at CONCUR2020
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.
Video talk on Gillian at PLDI 2020
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.
REMS and DeepSpec workshop, livestream talks
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.
Post-doc Position(s) Available
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.
PLDI 2020 song
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.
Paper accepted at PLDI 2020
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.
Papers accepted at ECOOP 2020
Apr 27, 2020
Two papers by members of the group have been accepted at the 34th European Conference on Object-Oriented Programming, ECOOP 2020.
Congratulations to Dr Shale Xiong
Feb 20, 2020
Many congratulations to Shale Xiong, who very successfully defended his PhD thesis, Parametric Operational Semantics for Consistency Models today.
Talk on Gillian, Workshop on High Assurance Systems Engineering, POPL2020
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
Six week programme Verified Software at the Isaac Newton Institute, Cambridge
Nov 11, 2019
Philippa Gardner is one of the organisers of the six week programme Verified Software at the Isaac Newton Institute, Cambridge.
Facebook testing and verification symposium, 20-21 November, livestream
Oct 30, 2019
The third annual Facebook testing and verification symposium will be held on 20-21 November in London.
Talk at Iris Workshop, Aarhus University, Denmark
Oct 28, 2019
Philippa Gardner, Emanuele D’Osualdo and Julian Sutherland attended the first edition of the Iris workshop.
Internship at Facebook, Infer Team
Oct 1, 2019
Julian Sutherland has just returned from a three months internship with the Facebook’s Infer team.
Workshop on Verified Software, Isaac Newton Institute for Mathematical Sciences, Cambridge.
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.
Goodbye to Jose Fragoso
Aug 15, 2019
Goodbye and good luck to Jose Fragoso, who is moving to the Instituto Superior Técnico, Lisbon, Portugal to become an Assistant Professor in the Department of Computer Science and Engineering.
Summer School Marktoberdorf 2019
Aug 9, 2019
Gaby Sampaio and Sacha Ayoun, two of the group’s PhD students, were invited to attend the 40th Marktoberdorf Summer School, organised by the Technical University of Munich (TUM).
Emanuele D'Osualdo and Shale Xiong, talks at Surrey Concurrency Workshop and S-REPLS
Jul 26, 2019
Emanuele D’Osualdo and Shale Xiong both gave talks at this year’s Surrey Concurrency Workshop and S-REPLS.
8th Conference on Algebra and Coalgebra in Computer Science
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.
Goodbye to Dr Andrea Cerone
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.
Talk at Formal Methods for Statistical Software workshop, Martin Bodin
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.
Paper accepted at ECOOP 2019
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)
Papers accepted at POPL 2019
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).
Facebook Continuous Reasoning research award for JaVerT 2.0.
Nov 7, 2018
Philippa Gardner, Jose Fragoso Santos and Petar Maksimovic have won a Facebook Continuous Reasoning research award for their project JaVerT 2.0: Automatic Compositional Analysis for JavaScript.
Welcome to Sacha Ayoun, new PhD student with the group
Oct 15, 2018
We are very happy to welcome Sacha Ayoun, who has joined the group as a PhD student.
IBM Project Prize to Radu Szasz, Msc project supervised by Philippa Gardner and Jose Fragoso
Sep 3, 2018
Congratulations to Radu Szasz (MEng Computing Year 4), who was awarded the IBM Project Prize for his MsC project, Typing JavaScript via Symbolic Execution, supervised by Philippa Gardner and Jose Fragoso.
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).
Congratulations to Emanuele D’Osualdo, Marie-Curie Fellowship
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.
Seminar by Felix Stutz on Automated Verification of Security Protocols
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.
Welcome to Martin Bodin, new member of the group
Jun 13, 2018
We are very happy to welcome Martin Bodin, who joins the group as a Research Associate. Martin did his PhD on Certified Semantics and Analysis of JavaScript at the University of Rennes 1 under the supervision of Alan Schmitt and Thomas Jensen. He then participated on the JSCert project to build a Coq specification for JavaScript.
Welcome to Felix Stutz
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.
Paper accepted and paper published
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.
Formal Methods Meets JavaScript Workshop
Mar 19, 2018
On Monday 19th March, we hosted a day of research talks on Programming Languages Formal Methods researchers on topics including language specification, program verification, etc. with a focus on research relating to the JavaScript language and ecosystem.
Congratulations to Dr Daiva Naudžiūnienė
Mar 1, 2018
Many congratulations to Daiva Naudžiūnienė, who very successfully defended her PhD thesis, An Infrastructure for Tractable Verification of JavaScript Programs on Monday 1st March.
Talk by Dr Justin Hsu, From Couplings to Probabilistic Relational Program Logics
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”.
Visitor to the group, Dr Chung-Kil Hur, Seoul National University.
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.
Welcome to Theotime Grohens, internship working on JaVert.
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.
Tech talk at Galois, Philippa Gardner
Jan 15, 2018
Philippa Gardner was invited to give a tech talk at Galois, Portland, USA on Javert, a JavaScript Verification Toolchain.
Paper presented at POPL18
Jan 12, 2018
José Fragoso Santos presented his paper JaVerT: JavaScript Verification using Separation Logic, jointly authored with Petar Maksimović, Daiva Naudžiūnienė, Thomas Wood and Philippa Gardner, at this year’s ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018).
PhD position, start date in October 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,
Google Compiler and Programming Language Summit, Munich, Germany
Dec 7, 2017
Gabriela Sampaio and Shale Xiong were two of the invited students attending this year’s Google Compiler and Programming Language Summit in Munich, Germany.
Visitor to the group, Siddharth Krishna, New York University, USA
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.
Visitor to the group, Giovanni Bernardi, IRIF, Paris
Nov 15, 2017
Dr Giovanni Bernardi of Paris Diderot University / IRIF visited the group in November to give a talk on his current work on must- testing for message passing concurrency.
Welcome to Gabriela Sampaio, new PhD student with the group
Oct 2, 2017
We are really happy to welcome Gabriela Sampaio, who has joined the group as a PhD student.
Paper accepted at POPL 2018
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).
Fifth Workshop on Formal Methods and Tools for Security (FMATS5)
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
Philippa Gardner gave a keynote talk entitled ‘Trustworthy Software Specification’ at the final event of the DFG-funded national research initiative “Reliably Secure Software Systems (RS3)”.
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.
Demo on the use of JaVerT at the JSTools'17 workshop
Jul 7, 2017
José Fragoso Santos gave a talk and demo on the use of JaVerT at the JSTools’17 workshop, part of this year’s European Conference on Object-Oriented Programming (ECOOP 2017).
Welcome to UROP students
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).
Paper accepted at Concur 2017
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.
Paper accepted at CSF'17
Jun 13, 2017
Emanuele D’Osualdo has had a paper accepted at this year’s Computer Security Foundations Symposium (CSF).
Philippa Gardner, invited talk at the Ecma TC39 meeting, Google, NY
May 25, 2017
Philippa Gardner was invited to give a talk about JavaScript Verification at the TC39 – ECMAScript Task group standards committee meeting held at Google, New York, this May.
Congratulations to Azalea Raad, joining the Max Planck Institute for Software Systems, Germany
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.
Goodbye to Dr Gian Ntzik, moving to Amadeus
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.
Johannes Kloos, visitor from MPI
May 9, 2017
Johannes Kloos, a fourth-year PhD student at the Max Planck Institute for Software Systems visited the group this week.
Visit to Aarhus University and Aarhus Concurrency Workshop
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
Philippa Gardner gave a talk on “A Concurrent Specification of PoSIX” at the open workshop “Consistency in distributed storage”. organised by Marc Shapiro (UPMC-LIP6 and Inria).
Visitor to the group, Dr Azadeh Farzan of the University of Toronto, Canada
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.
Keynote address at IPM FSEN Conference 2017, Iran
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.
Welcome to Emanuele D'Osualdo, new member of the group
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.
Visit from Alan Schmitt, Inria, France
Feb 20, 2017
Alan Schmitt, a researcher in the Celtique team at Inria in Rennes visited the group this week. Alan’s research focuses on the certification of semantics and static analyses, in particular the semantics of JavaScript and analyses based on abstract interpretation.
National Cyber Security Centre (NCSC) official opening
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.
Third edition of the Introduction to Verification and Testing (INVEST) workshop
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.
Congratulations to Azalea Raad on her viva
Feb 10, 2017
Congratulations to Azalea Raad who very successfully defended her PhD thesis, Abstraction, Refinement and Concurrent Reasoning on Friday 10 February.
Papers accepted at ESOP 2017
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.
Congratulations to Gian Ntzik on his viva
Feb 1, 2017
Congratulations to Gian Ntzik on successfully defending his PhD thesis, Reasoning about POSIX File Systems and many thanks to Ally Donaldson and Hongseok Yang who acted as examiners.
Talk at Principles in Practice (PiP), POPL 2017
Jan 20, 2017
Philippa gave a talk entitled An Infrastructure for Tractable Verification of JavaScript Programs at this year’s Principles in Practice workshop (PiP).
Successful viva for Pedro da Rocha Pinto
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.
Visit from Julian Dolby, IBM
Dec 15, 2016
Julian Dolby, a researcher at IBM’s Thomas J. Watson Research Center in New York visited the VTSS group for a week in December.
JSExplain discussed at ECMAScript standards committee meeting
Dec 5, 2016
Thomas Wood attended the latest ECMAScript standards committee TC39 meeting this November in San Francisco.
Talk at Dagstuhl Seminar
Nov 23, 2016
Andrea Cerone was invited to attend the seminar on Concurrency with Weak Memory Models at Schloss Dagstuhl last week.
Infer Lab at Imperial
Nov 14, 2016
The Separation Logic course team ran a lab on Infer, an automatic verification tool based on separation logic, developed at Facebook where it is used every day to verify millions of lines of code.
Keynote talk at the IET SSCS Conference
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.
Papers published by Azalea Raad
Oct 3, 2016
Azalea Raad has had two papers published in Programming Languages and System: Proceedings of the 14th Asian Symposium, APLAS 2016.
Daiva Naudžiūnienė moving to Facebook
Sep 15, 2016
Congratulations to Daiva Naudžiūnienė, who is off to work for Facebook in the new year.
Welcome to Andrea Cerone, new member of the group
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.
One new postdoc position at Imperial College
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.