Publications

BibTex format

@inproceedings{Sampaio:2020:10.4230/LIPIcs.ECOOP.2020.28,
author = {Sampaio, G and Fragoso, Santos J and Maksimovic, P and Gardner, P},
doi = {10.4230/LIPIcs.ECOOP.2020.28},
pages = {28:1--28:29},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik},
title = {A trusted infrastructure for symbolic analysis of event-driven web applications},
url = {http://dx.doi.org/10.4230/LIPIcs.ECOOP.2020.28},
year = {2020}
}

Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - We introduce a trusted infrastructure for the symbolic analysis of modern event-driven Web applica-tions. This infrastructure consists of reference implementations of the DOM Core Level 1, DOM UIEvents, JavaScript Promises and the JavaScriptasync/awaitAPIs, all underpinned by a simpleCore Event Semantics which is sufficiently expressive to describe the event models underlying theseAPIs. Our reference implementations are trustworthy in that three follow the appropriate standardsline-by-line and all are thoroughly tested against the official test-suites, passing all the applicabletests. Using the Core Event Semantics and the reference implementations, we develop JaVerT.Click,a symbolic execution tool for JavaScript that, for the first time, supports reasoning about JavaScriptprograms that use multiple event-related APIs. We demonstrate the viability of JaVerT.Click byproving both the presence and absence of bugs in real-world JavaScript code.
AU  - Sampaio,G
AU  - Fragoso,Santos J
AU  - Maksimovic,P
AU  - Gardner,P
DO  - 10.4230/LIPIcs.ECOOP.2020.28
EP  - 1
PB  - Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
PY  - 2020///
SN  - 1868-8969
SP  - 28
TI  - A trusted infrastructure for symbolic analysis of event-driven web applications
UR  - http://dx.doi.org/10.4230/LIPIcs.ECOOP.2020.28
UR  - http://hdl.handle.net/10044/1/79710
ER  -

Download

ProfessorPhilippaGardner

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)