JaVerT 2.0: compositional symbolic execution for JavaScript
File(s)popl19main-p189-p.pdf (1.04 MB)
Published version
OA Location
Author(s)
Fragoso Santos, Jose
Maksimovic, Petar
Cunha Sampaio, Gabriela
Gardner, Philippa
Type
Conference Paper
Abstract
We propose a novel, unified approach to the development of compositional symbolic execution tools, bridging the gap between classical symbolic execution and compositional program reasoning based on separation logic. Using this approach, we build JaVerT 2.0, a symbolic analysis tool for JavaScript that follows the language semantics without simplifications. JaVerT 2.0 supports whole-program symbolic testing, verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback to the developer during whole-program symbolic testing and guides the inference of resource of the bi-abductive execution. We evaluate the performance of JaVerT 2.0 on a number of JavaScript data-structure libraries, demonstrating: the scalability of our whole-program symbolic testing; an improvement over the state-of-the-art in JavaScript verification; and the feasibility of automatic compositional testing for JavaScript.
Date Issued
2019-01-02
Date Acceptance
2018-10-09
Citation
Proceedings of the ACM on Programming Languages, 2019, 3, pp.66:1-66:31
ISSN
2475-1421
Publisher
Association for Computing Machinery
Start Page
66:1
End Page
66:31
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
3
Copyright Statement
© 2019 Copyright held by the owner/author(s). This work is licenced under a Creative Commons Attribution-Non-Commercial 4.0 International licence (https://creativecommons.org/licenses/by-nc/4.0/)
Sponsor
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (E
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
EP/K008528/1 - RG65358
EP/K008528/1
EP/K032089/1
EP/R034567/1
Source
ACM SIGPLAN Symposium on Principles of Programming Languages (POPL)
Publication Status
Published
Start Date
2019-01-13
Finish Date
2019-01-19
Coverage Spatial
Cascais, Portugal