Philippa Gardner is a professor in the Department of Computing at Imperial College London and leader of the Verified Trustworthy Software Specification Group. Her current research focusses on program verification: in particular, reasoning about Web programs (JavaScript and DOM); and reasoning about concurrent programs.

She completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh in 1992. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship from 2005 to 2010 at Imperial.

Philippa directs the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC, from 2017 to 2022. She also chairs the BCS awards committee, which decides the Lovelace medal (senior) and Roger Needham award (mid-career) for computer science and engineering.


News Archive

Research Group

Please click here for more information about Philippa’s research group.

Full Bibliography

Publications and PhD Theses

  1. JaVerT: JavaScript verification toolchain

    • José Fragoso Santos
    • Petar Maksimović
    • Daiva Naudžiūnienė
    • Thomas Wood
    • Philippa Gardner


    PACMPL, vol. 2(POPL), pp. 50:1–50:33

  2. Verified trustworthy software systems

    • Philippa Gardner

    Sep 2017

    Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, vol. 375(2104)

  3. Towards Logic-based Verification of JavaScript Programs

    • José Fragoso Santos
    • Philippa Gardner
    • Petar Maksimović
    • Daiva Naudžiūnienė

    Aug 2017

    Proceedings of 26th Conference on Automated Deduction (CADE 26)

  4. Abstraction, Refinement and Concurrent Reasoning

    • Azalea Raad

    Jun 2017

    Ph.D. Thesis, Imperial College London

  5. Reasoning with Time and Data Abstractions

    • Pedro da Rocha Pinto

    May 2017

    Ph.D. Thesis, Imperial College London

Full Bibliography

Invited Talks


  • `Verification and Testing for JavaScript’, invited talk at the first Facebook Testing and Verification Symposium, Facebook, London, UK.
  • `Trustworthy Software Specification’, keynote, final conference for the DFG priority program ‘Reliably Secure Software Systems (RS3)’, Darmstadt, Germany.
  • `JaVerT: The JavaScript Verification Toolchain’, keynote, International Conference on Automated Reasoning (CADE), Gothenburg, Sweden.
  • `Verified Trustworthy Software Systems’, invited talk, workshop on Challenges in Industry and Research at the Alan Turing Institute as part of the the Newton Institute programme on Big Proof, London, UK.
  • `Towards Trustworthy Verification of JavaScript’, invited talk at the Emerging technologies session, TC39: ECMAScript Task group standards committee meeting, New York, USA.
  • `A Concurrent Specification of POSIX’, invited talk at Shapiro’s RainbowFS Workshop on Consistency in Distributed Systems, Paris, France.
  • `Tractable Verification of JavaScript Programs’, keynote talk at FSEN’17, Tehran, Iran.
  • `Understanding and Verifying JavaScript Programs’, UPMC Informatics Colloquium (Distinguished Seminar Series), Paris, France.
  • `Tractable Verification of JavaScript Programs’ invited talk on JSVerify at the workshop on Principles in Practice, POPL’17, Paris, France.


  • ‘Verified Trustworthy Software Systems’, keynote talk at 11th System Safety and Cyber Security Conference, IET, London, UK.
  • ‘Scalable reasoning about Concurrent programs’, invited talk and participant at the IFIP WG 1.9/2.15 working group on Verified Software, Montauban, France.
  • ‘A Concurrent Specification of POSIX’, invited talk, workshop on Trends in Concurrency Theory (TRENDS 2016), CONCUR, Quebec, Canada.
  • ‘An Intermediate Language and Compiler for JavaScript Verification’, invited talk at JSTools workshop associated with ECOOP’16, Rome, Italy.
  • ‘JavaScript and Concurrency Verification’, invited talk, the first workshop on DeepSpec: The Science of Deep Specification, Princeton, USA (with Petar Maksimovic).
  • ‘A Concurrent Specification of POSIX’, invited talk, Dagstuhl seminar on ‘Synergies among Testing, Verification and Repair for Concurrent Programs’,Dagstuhl, Germany.
  • ‘Understanding and Verifying JavaScript Programs’, talk at the Royal Society Discussion and Scientific meeting on ‘Verified trustworthy software systems’, Royal Society, London, UK.


  • ‘Understanding and Verifying JavaScript programs’, invited talk, Google EU Compiler Summit’15, Munich, Germany.
  • ‘Understanding and Verifying JavaScript programs’, invited talk, Departmental seminar at Cambridge, UK.
  • ‘Research Institute in Automated Program Analysis and Verification’, invited talk, UK Cyber Security Research Conference, London, UK.
  • Seminar on Open Problems in Concurrency, organised by ICFP, Bertinoro, Italy.
  • ‘A Trusted Mechanised Specification of JavaScript: One Year On’, keynote talk at CAV’15, San Francisco, USA.
  • ‘Modern Concurrent Separation Logics’, invited tutorial at the Mathematical Foundations of Programming Semantics, Nijmegen, Netherlands.


  • Workshop on the Certification of High-level and Low-level Programs, Invited talk, Paris, France.
  • Workshop on Higher-order Programming with Effects (HOPE 2014), Keynote, associated with ICFP, Gothenburg, Sweden.
  • JSTools 2014, Invited talk, associated with ECOOP, Uppsala, Sweden.
  • Seminar on Open Problems in Concurrency, Bertinoro, organised by ICFP Departmental seminars at Kent, York and Oxford, Bertinoro, Italy.
  • ‘A Trusted Mechanised Specification of the JavaScript Standard’, Departmental Seminar, Oxford University, UK.
  • Departmental seminars at Kent, York and Oxford, UK.


I teach the following courses:

I am keen to supervise undergraduate and M.Sc projects.


  • 2017–2022 EPSRC Grant: Research Institute in Verified Trustworthy Software Systems, PI, £798,000.
  • 2013–2019 EPSRC Programme Grant: REMS: Rigorous Engineering for Mainstream Systems, CI (Sewell, PI, Cambridge), £1,349,302.
  • 2015–2016 Facebook Faculty Grant, $40,000
  • 2013–2016 EPSRC Grant: Certified Verification of Client-side Web Programs, PI, £627,463.
  • 2013–2016 EPSRC and GCHQ Grant: Research Institute in Automated Program Analysis and Verification, PI, £266,461.
  • 2010–2016 EPSRC Programme Grant: Resource Reasoning, CI (O’Hearn, PI, UCL), £1,536,661.
  • 2006–2010 EPSRC Grant: Smallfoot: Static Assertion Checking for C Programs, CI (O’Hearn, PI, Queen Mary), £330,000.
  • 2006–2009 BBSRC Grant: Applying Techniques from Process Algebra to Model Cell Behaviour, PI, £155,146.
  • 2004–2007 EPSRC E-science Grant: Dynamic Net Data: Theory and Experiment, PI, £241,438.
  • 2003–2006 EPSRC responsive-mode Grant: Spatial Logics for Querying Graphs, PI, £171,916.
  • 2002–2004 Microsoft research Grant: Querying Data on the Web, £34,000.
  • 1998–2001 EPSRC Grant: Calculi for Interaction: Theory and Experiment, CI (Milner, PI), £279,899.

Awards and Fellowships

  • 2013 President and Rector’s Award for Excellence in Teaching, a prestigious Imperial teaching award.
  • 2005–2009 Microsoft Research — Royal Academy of Engineering Senior Research Fellowship, Imperial, £362,272.
  • 2007 Rector’s bonus for Research, a prestigious Imperial research award, Imperial, 2007, £10.000.
  • 1997-2002 EPSRC Advanced Fellowship, Operational Models of Computation, Cambridge and Imperial, £149,996.
  • 1994–1996 The Royal Society of Edinburgh — BP Research Fellowship, Edinburgh, £143,000.
  • 1992–1993 Science and Engineering Research Council Postdoctoral Fellowship, Edinburgh, £73,000.



Philippa Gardner

  • (substitute xx for @)
  • +44 (0)20 7594 48292

Teresa Carbajo Garcia

Administrative Program Manager


  • Department of Computing
    180 Queen's Gate
    South Kensington Campus
    Imperial College London
    SW7 2AZ