Detail

JaVerT: JavaScript Verification Toolchain

The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification. We will present JaVerT, a semi-automatic JavaScript Verification Toolchain, based on separation logic and aimed at the specialist developer wanting rich, mechanically verified specifications, of critical JavaScript code. We will describe the JaVerT verification pipeline, focusing on: JS-2-JSIL, a well-tested compiler from JavaScript to JSIL, an intermediate goto language well suited for verification; and JSIL Verify, a semi-automatic verification tool based on a sound program logic for JSIL. We illustrate how JaVerT can be used to specify and verify JavaScript data structure libraries written in object-oriented style using the example of a JavaScript implementation of a key-value map. Finally, we will show how to use standard symbolic execution techniques for debugging JaVerT specifications in order to find concrete witnesses for bugs in both specification and code. Further details can be found in the eponymous paper to be presented at POPL’18.