We develop compositional reasoning techniques for concurrent programs using modern concurrent separation logics, introducing
fundamental concepts in the reasoning: logical abstraction (Concurrent Abstract Predicates), logical atomicity (the TaDA Logic) and logical environment liveness properties (TaDA Live). In addition, we have started to work on weak consistency models for distribution, developing an interleaving operational semantics for client-observational behaviour of atomic transactions (ECOOP’20).
We have applied our reasoning to, for example, algorithms for
manipulating concurrent B-trees, skip lists from
...
...
@@ -25,15 +20,16 @@ logics, and applying our work to real-world concurrent programs.
#### Research Support
This research is supported by the EPSRC programme grant
This research is supported by Gardner's UKRI Established Career Fellowship
["VeTSpec: Verified Trustworthy Software Specification"][VeTSpec] and
Emanuele D'Osualdo's Marie-Curie Fellowship "VeSPA: Verification through
Security and Progress Abstractions".
It was previously supported by the EPSRC programme grant
[EP/K008528/1]:[REMS: Rigorous Engineering of Mainstream
Systems][REMS] and previously by the EPSRC programme grant [EP/H008373/2]: [Resource
Reasoning]. We also have substantial collaboration with [Thomas Dinsdale-Young],
previously a PhD student and RA of Gardner and now an independent
research fellow at the University of Aarhus.
Systems][REMS] and the EPSRC programme grant [EP/H008373/2]: [Resource
We study the mechanised specification of the JavaScript language
(following the ECMAScript 5 standard) and the verification of
JavaScript programs.
We study various forms of program analysis for JavaScript (ECMAScript 5 Strict) programs,
extending this work to include important Web APIs, such as the DOM (including UI Events), JavaScript Promises, and async/await.
We are also interested in the mechanised specification of JavaScript itself.
#### JSCert
#### 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][https://kenwheeler.github.io/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][https://github.com/sindresorhus/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](http://jscert.org/), 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. We are currently extending this specification to the
numerous libraries, providing continuous test integration for the
ever-growing specification, developing a new, human-readable JSRef,
with a tighter connection to the standard and good tracking
properties, and creating the web service Explain.js to explain
behavioural complexities of JavaScript programs.
#### JSIL
We have developed a principled compiler from JavaScript (ECMAScript 5
strict) to a small intermediate language JSIL, which has a simpler
operational semantics and is better suited to program verification.
The compiler has been substantially tested using the Test262 test
suite and it comes with a hand-proof of translation correctness
for a fragment of the language. We will use JSIL to develop JSVerify - a
verification tool for JavaScript. Daiva Naudžiūnienė will
this year hold internships at Amazon and Facebook to use
JSIL to develop front-ends for the CBMC and Infer verification tools.
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 research is supported by the EPSRC
This work is supported by Gardner's UKRI Established Career Fellowship
