Repository logo
  • Log In
    Log in via Symplectic to deposit your publication(s).
Repository logo
  • About
  • Communities & Collections
  • Advanced Search
  • Statistics
  • Log In
    Log in via Symplectic to deposit your publication(s).
  1. Home
  2. Faculty of Engineering
  3. Faculty of Engineering
  4. JaVerT 2.0: compositional symbolic execution for JavaScript
 
  • Details
JaVerT 2.0: compositional symbolic execution for JavaScript
File(s)
popl19main-p189-p.pdf (1.04 MB)
Published version
OA Location
https://doi.org/10.1145/3290379
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
URI
http://hdl.handle.net/10044/1/65406
DOI
https://www.dx.doi.org/10.1145/3290379
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
About
Spiral Depositing with Spiral Publishing with Spiral Symplectic
Contact us
Open access team Report an issue
Other Services
Scholarly Communications Library Services
logo

Imperial College London

South Kensington Campus

London SW7 2AZ, UK

tel: +44 (0)20 7589 5111

Accessibility Modern slavery statement Cookie Policy

Built with DSpace-CRIS software - Extension maintained and optimized by 4Science

  • Cookie settings
  • Privacy policy
  • End User Agreement
  • Send Feedback