Verified Software

We study the testing and verification of JavaScript programs and Web APIs, and mechanised language specification using JavaScript as the real-world example language.

JaVerT

We have developed JaVerT, a compositional symbolic analysis tool for JavaScript, targeting the strict mode of the ECMAScript 5 standard. JaVerT supports whole-program symbolic testing, verification and automatic compositional testing based on bi-abduction. It comprises:

• JSIL, an intermediate goto language with a symbolic execution engine with explicit management of execution errors that guides the feedback for symbolic testing and the automatic bi-abductive inference. The meta-theory underpinning JSIL is formally defined and modular, streamlining the proofs and guiding the implementation.
• JS-2-JSIL, a trusted compiler that preserves the JavaScript memory model and semantics, trusted in the sense that it is line-by-line close to the standard and comprehensively tested using the official Test262 test suite.

Web APIs

Using our considerable experience with the DOM specification and JavaScript analysis, we have recently (ECOOP’20) introduced a trusted infrastructure for symbolic analysis of modern event-driven Web applications, comprising:

• reference implementations of the DOM Core Level 1, DOM UI Events, JavaScript Promises, and the JavaScript async/await APIs, all following the API standards as closely as possible and all thoroughly tested against the official test suites;
• a simple Core Events Semantics that is sufficiently expressive to describe the event models underlying these APIs;
• JaVerT.Click, an extension of JaVerT with the Core Events Semantics, that is, for the first time, able to symbolically test JavaScript programs that use any/all of the above-mentioned APIs.

We have used JaVerT.Click to analyse the events module of cash, a small, widely-used jQuery alternative, in which we found two bugs (fixed) and for which we have proven boundned correctness of several essential properties, such as “an event handler can be triggered if and only if it has previously been registered”. We have also found a bug in the p-map library (fixed), which extends the functionality of JavaScript Promises.

Language Semantics

With Bodin, Charguéraud, and Schmitt at Inria, we have developed JSCert, a substantial Coq specification that is line-by-line close to the core language of the ECMAScript 5 standard. It comes with a reference interpreter, JSRef, proven correct with respect to JSCert and tested using the official Test262 test suite. With Schmitt and Jensen, we have also recently introduced the skeletal semantics framework for capturing both concrete and abstract semantics, connected together by a general consistency result. Our hope is that this framework will simplify the verification of properties such has heap well-formedness for large complex languages such as JavaScript.

Research Support

This work is supported by Gardner’s UKRI Established Career Fellowship “VeTSpec: Verified Trustworthy Software Specification”. It was previously supported by the EPSRC programme grant EP/K008528/1: REMS: Rigorous Engineering of Mainstream Systems, the EPSRC/GCHQ grant EP/K032089/1: Certified Verification of Client-Side Web Programs, and the EPSRC programme grant EP/H008373/2: Resource Reasoning. We also have substantial collaboration with José Fragoso Santos, previously an RA in the group and now an Assistant Professor at the Instituto Superior Técnico, Lisbon.

People

Recent Publications

1. A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications

   • Gabriela Sampaio
   • José Fragoso Santos
   • Petar Maksimovic
   • Philippa Gardner

   Proceedings of the 34^th European Conference on Object-Oriented Programming (ECOOP 2020)

2. JaVerT 2.0: Compositional Symbolic Execution for JavaScript

   • José Fragoso Santos
   • Petar Maksimovic
   • Gabriela Sampaio
   • Philippa Gardner

   Proceedings of the 46^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’19), vol. 3( POPL)

3. Skeletal Semantics and their Interpretations

   • Martin Bodin
   • Philippa Gardner
   • Thomas Jensen
   • Alan Schmitt

   Proceedings of the 46^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’19)

4. Symbolic Execution for JavaScript

   • José Fragoso Santos
   • Petar Maksimovic
   • Théotime Grohens
   • Julian Dolby
   • Philippa Gardner

   Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pp. 11:1–11:14

5. JaVerT: JavaScript Verification and Testing Framework: Invited Talk

   • Philippa Gardner

   Proceedings of the 20^thh International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, pp. 1:1–1:4

6. JSExplain: a Double Debugger for JavaScript

   • Arthur Charguéraud
   • Alan Schmitt
   • Thomas Wood

   WWW ’18 Companion: The 2018 Web Conference Companion, April 23–27, 2018, Lyon, France

7. JaVerT: JavaScript Verification Toolchain

   • José Fragoso Santos
   • Petar Maksimovic
   • Daiva Naudziuniene
   • Thomas Wood
   • Philippa Gardner

   Proceedings of the 45^th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’18), pp. 50:1–50:33

8. An Infrastructure for Tractable Verification of JavaScript Programs

   • Daiva Naudziuniene

   Ph.D. Thesis, Imperial College London

9. Towards Logic-based Verification of JavaScript Programs

   • José Fragoso Santos
   • Philippa Gardner
   • Petar Maksimovic
   • Daiva Naudziuniene

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

10. DOM: Specification and Client Reasoning

    • Azalea Raad
    • José Fragoso Santos
    • Philippa Gardner

    Proceedings of the 13^th Asian Symposium on Programming Languages and Systems (APLAS’16), pp. 401–422