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


  • 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 PSVG 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.