JaVerT 2.0: compositional symbolic execution for JavaScript
- Submitting institution
-
Imperial College of Science, Technology and Medicine
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 2267
- Type
- E - Conference contribution
- DOI
-
10.1145/3290379
- Title of conference / published proceedings
- Proceedings of the ACM on Programming Languages
- First page
- 66:1
- Volume
- 3
- Issue
- POPL
- ISSN
- 2475-1421
- Open access status
- Compliant
- Month of publication
- January
- Year of publication
- 2019
- URL
-
-
- Supplementary information
-
10.1145/3290379
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
3
- Research group(s)
-
-
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- JaVerT 2.0 improved performance over the state-of-the-art JaVerT verification tool (POPL'18; https://dl.acm.org/doi/10.1145/3158138) and the Cosette symbolic-testing tool (PPDP'18; https://doi.org/10.1145/3236950.3236956). It found bugs, which were fixed, in the Buckets.js library, and verified parts of the serialisation module for the AWS encryption SDK message format (https://vtss.doc.ic.ac.uk/research/javascript.html). An ECOOP'20 paper (https://drops.dagstuhl.de/opus/volltexte/2020/13185/) extends JaVerT 2.0 to event-driven Web APIs, finding bugs and proving correctness results. Our work led to funding of a UKRI Established Fellowship (EP/R034567/1; £1.5M) and from Facebook ($40K). It resulted in invited talks at CADE'17 (https://bit.ly/2zAk08j), FSEN'17 (http://fsen.ir/2017/KeynoteSpeakers.aspx), Facebook Testing/Verification Symposium'17 (https://bit.ly/2LZ1CZj) and PPDP’18 (https://bit.ly/2B502D5). Passed POPL’19 Artifact evaluation.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
