The dynamic nature of JavaScript, together with its complex semantics, makes it a difficult target for logic-based verification techniques. We present JaVerT: a semi-automatic verification tool chain for JavaScript based on separation logic. We target functionally correct specifications of critical JavaScript software, in particular focusing on small Node.js libraries that have high usability: for example, those describing well-known data structures, such as a priority queue. JaVerT provides a wide variety of built-in abstractions so that our specifications are straightforward, despite the underlying complexity of the JavaScript semantics.

The talk will consist of a demo of JaVerT, illustrating how it can be used to specify and verify a JavaScript priority queue implementation. It will showcase the abstractions provided by JaVerT for reasoning about the JavaScript semantics, with an emphasis on objects, prototype chains, and function closures, as well as the infrastructure for supporting arbitrary user-defined recursive predicates.