JaVerT - JavaScript Verification Toolchain for Logic-Based Program Analysis

Watch a 24-minute conference presentation from POPL 2018 exploring JaVerT, a semi-automatic JavaScript Verification Toolchain developed for logic-based verification of critical JavaScript code. Learn how this toolchain implements separation logic to help specialist developers create mechanically verified specifications through key abstractions of JavaScript heap structures like prototype chains and function closures. Discover the three main components of the verification pipeline: JS-2-JSIL compiler, JSIL Verify semi-automatic verification tool, and verified axiomatic specifications of JavaScript internal functions. See practical demonstrations of JaVerT being used to verify functional correctness properties across various applications including object-oriented data structure libraries, binary search trees, list operations, function closure examples, and official ECMAScript test cases. Understand how this toolchain makes it feasible to reason about and verify increasingly complex JavaScript code through its innovative approach to handling JavaScript's dynamic nature and complex semantics.