Fri 12 Jan 2018 10:55 - 11:20 at Watercourt - Dynamic Languages Chair(s): Jean Yang

The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification. We introduce JaVerT, a semi-automatic JavaScript Verification Toolchain based on separation logic. To specify JavaScript programs, we design abstractions that capture its key heap structures (e.g. prototype chains, function closures), allowing the user to write clear and succinct specifications with minimal knowledge of the JavaScript internals. To verify JavaScript programs, we develop JaVerT, a verification pipeline consisting of: JS-2-JSIL, a well-tested compiler from JavaScript to JSIL, an intermediate goto language capturing the fundamental dynamic features of JavaScript; JSIL Verify, a semi-automatic verification tool based on a sound JSIL separation logic; and verified axiomatic specifications of the JavaScript internal functions. Using JaVerT, we verify functional correctness properties of data-structure libraries (key-value map, priority queue) written in object-oriented style; operations on data structures such as BSTs and lists; examples illustrating function closures; and test cases from the official ECMAScript test suite. The verification times suggest that reasoning about larger, more complex code using JaVerT is feasible.

Fri 12 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

10:30 - 12:10: Research Papers - Dynamic Languages at Watercourt
Chair(s): Jean YangCarnegie Mellon University
POPL-2018-papers10:30 - 10:55
Olivier FlückigerNortheastern University, USA, Gabriel SchererNortheastern University, USA, Ming-Ho YeeNortheastern University, USA, Aviral GoelNortheastern University, Amal AhmedNortheastern University, USA, Jan VitekNortheastern University
DOI Pre-print
POPL-2018-papers10:55 - 11:20
José Fragoso SantosImperial College London, Petar MaksimovićImperial College London, Daiva NaudžiūnienėImperial College London, Thomas WoodImperial College London, Philippa GardnerImperial College London
POPL-2018-papers11:20 - 11:45
Phúc C. NguyễnUniversity of Maryland, Thomas GilrayUniversity of Maryland, Sam Tobin-HochstadtIndiana University, David Van HornUniversity of Maryland
POPL-2018-papers11:45 - 12:10
Nada AminUniversity of Cambridge, Tiark RompfPurdue University