Imperial College London
Alternate

ProfessorPhilippaGardner

Faculty of Engineering, Department of Computing

Professor of Theoretical Computer Science
 
 
 
//

Contact

 

+44 (0)20 7594 8292p.gardner Website

 
 
//

Location

 

453Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Fragoso:2019:10.1145/3290379,
author = {Fragoso, Santos J and Maksimovic, P and Cunha, Sampaio G and Gardner, P and Faustino, Fragoso Femenin Dos Santos J and Maksimovic, P and Gardner, P and Sampaio, G},
doi = {10.1145/3290379},
pages = {66:1--66:31},
publisher = {Association for Computing Machinery},
title = {JaVerT 2.0: compositional symbolic execution for JavaScript},
url = {http://dx.doi.org/10.1145/3290379},
year = {2019}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - Fragoso,Santos J
AU  - Maksimovic,P
AU  - Cunha,Sampaio G
AU  - Gardner,P
AU  - Faustino,Fragoso Femenin Dos Santos J
AU  - Maksimovic,P
AU  - Gardner,P
AU  - Sampaio,G
DO  - 10.1145/3290379
EP  - 1
PB  - Association for Computing Machinery
PY  - 2019///
SN  - 2475-1421
SP  - 66
TI  - JaVerT 2.0: compositional symbolic execution for JavaScript
UR  - http://dx.doi.org/10.1145/3290379
UR  - http://hdl.handle.net/10044/1/65406
ER  -
Download