Ph.D. Thesis, Imperial College London

Publication Year




The highly dynamic nature of JavaScript, coupled with its intricate semantics, makes the understanding and development of correct JavaScript code notoriously dificult. We believe that logic-based verification has much to offer to JavaScript. In particular, separation logic has been successfully applied to verification tools for static languages. However, it has hardly been used to reason about programs written in dynamic languages in general, and JavaScript in particular. This thesis presents JaVerT, a semi-automatic JavaScript Verification Toolchain for tractable logicbased verification of JavaScript programs. JaVerT verifies JavaScript programs annotated with function specifications in the form of pre- and postconditions, loop invariants, and annotations for the folding and unfolding of user-defined predicates. We design natural JavaScript abstractions that allow JavaScript developers wishing to verify JavaScript programs to not think about almost any internals of the language. The actual process of how JaVerT verifies the given annotated JavaScript program is not visible to the JavaScript developer, and is achieved using our JSIL verification infrastructure. This infrastructure includes: JSIL, a simple goto language, suitable for logic-based verification of JavaScript; JSIL Logic, a sound separation logic for JSIL; and JSIL Verify, a semi-automatic verification tool, based on JSIL Logic. The joining ingredient of JaVerT is a JavaScript frontend to our JSIL verification infrastructure, tightly connecting programs and reasoning at the level of JavaScript to programs and reasoning at the level of JSIL. This frontend includes a well-tested compiler from JavaScript code to JSIL code, a translator from JavaScript Logic to JSIL Logic, and well-tested JSIL reference implementations and verified axiomatic specifications of the JavaScript internal functions. We demonstrate the feasibility of JaVerT to specify and verify simple data structure libraries, illustrating our ideas using an implementation of a priority queue. Our given specifications ensure prototype safety of library operations, in that they describe the conditions under which these operations exhibit the desired behaviour.

Source Materials