Cosette: Symbolic Execution for JavaScript

Published at PPDP 2018
DOI: 10.1145/3236950.3236956

Authors

• José Fragoso Santos
• Petar Maksimović
• Daiva Naudžiūnienė
• Thomas Wood
• Philippa Gardner

Abstract

We present a framework for trustworthy symbolic execution of JavaScripts programs, whose aim is to assist developers in the testing of their code: the developer writes symbolic tests for which the framework provides concrete counter-models. We create the framework following a new, general methodology for designing compositional program analyses for dynamic languages. We prove that the underlying symbolic execution is sound and does not generate false positives. We establish additional trust by using the theory to precisely guide the implementation and by thorough testing. We apply our framework to whole-program symbolic testing of real-world JavaScript libraries and compositional debugging of separation logic specifications of JavaScript programs.