Commit 5abc7a7b authored by pmaksimo's avatar pmaksimo

minor

parent 1aad95a4
Pipeline #142112 passed with stages
in 4 minutes and 17 seconds
...@@ -15,15 +15,15 @@ We are also interested in the mechanised specification of JavaScript itself. ...@@ -15,15 +15,15 @@ We are also interested in the mechanised specification of JavaScript itself.
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. - 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. - 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 #### 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; - 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; - 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. - 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 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".
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment