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

Software contracts allow programmers to state rich program properties using the full expressive power of an object language. However, since they are enforced at runtime, monitoring contracts imposes significant overhead and delays error discovery. So contract verification aims to guarantee all or most of these properties ahead of time, enabling valuable optimizations and yielding a more general assurance of correctness. Existing methods for static contract verification satisfy the needs of more restricted target languages, but fail to address the challenges unique to those conjoining untyped, dynamic programming, higher-order functions, modularity, and statefulness. Our approach tackles all these features at once, in the context of the full Racket system—a mature environment for stateful, higher-order, multi-paradigm programming with or without types. Evaluating our method using a set of both pure and stateful benchmarks, we are able to verify 99.94% of checks statically (all but 28 of 51, 713).

Stateful, higher-order functions pose significant challenges for static contract verification in particular. In the presence of these features, a modular analysis must permit code from the current module to escape permanently to an opaque context (unspecified code from outside the current module) that may be stateful and therefore store a reference to the escaped closure. Also, contracts themselves, being predicates written in unrestricted Racket, may exhibit stateful behavior; a sound approach must be robust to contracts which are arbitrarily expressive and interwoven with the code they monitor. In this paper, we present and evaluate our solution based on higher-order symbolic execution, explain the techniques we used to address such thorny issues, formalize a notion of behavioral approximation, and use it to provide a mechanized proof of soundness.

Fri 12 Jan
Times are displayed in time zone: Tijuana, Baja California change

10:30 - 12:10: Dynamic LanguagesResearch Papers at Watercourt
Chair(s): Jean YangCarnegie Mellon University
10:30 - 10:55
Correctness of Speculative Optimizations with Dynamic Deoptimization
Research Papers
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
10:55 - 11:20
JaVerT: JavaScript Verification Toolchain
Research Papers
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
11:20 - 11:45
Soft Contract Verification for Higher-order Stateful Programs
Research Papers
Phúc C. NguyễnUniversity of Maryland, Thomas GilrayUniversity of Maryland, Sam Tobin-HochstadtIndiana University, David Van HornUniversity of Maryland
11:45 - 12:10
Collapsing Towers of Interpreters
Research Papers
Nada AminUniversity of Cambridge, Tiark RompfPurdue University