• Talk at 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 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.
    The viva was passed with minor corrections. Many thanks to Aleksandar Nanevski and Viktor Vafeiadis who acted as external examiner and to Susan Eisenbach, who acted as the internal examiner.


  • 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. Julian’s research focuses on static program analysis, software testing and the semantic web and during his visit, Julian worked with José Fragoso and Petar Maksimovic in a symbolic analysis for JavaScript based on JSIL and Rosette with the end goal of having a bug-finding tool for JavaScript.


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