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).
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
@@ -11,14 +11,14 @@ We study the testing and verification of JavaScript programs and Web APIs, and m
#### 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:
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:
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;
