Cosette

Symbolic Execution For JavaScript

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.

Venue

International Symposium on Principles and Practice of Declarative Programming (PPDP)

Year

2018

DOI