2026-07-22T07:15:38Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13185 2024-03-06T10:49:56Z ddc:004 open_access

A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications Sampaio, Gabriela Fragoso Santos, José Maksimović, Petar Gardner, Philippa Events DOM JavaScript promises symbolic execution bug-finding We introduce a trusted infrastructure for the symbolic analysis of modern event-driven Web applications. This infrastructure consists of reference implementations of the DOM Core Level 1, DOM UI Events, JavaScript Promises and the JavaScript async/await APIs, all underpinned by a simple Core Event Semantics which is sufficiently expressive to describe the event models underlying these APIs. Our reference implementations are trustworthy in that three follow the appropriate standards line-by-line and all are thoroughly tested against the official test-suites, passing all the applicable tests. 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 JavaScript programs that use multiple event-related APIs. We demonstrate the viability of JaVerT.Click by proving both the presence and absence of bugs in real-world JavaScript code. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Gabriela Sampaio and José Fragoso Santos and Petar Maksimović and Philippa Gardner 2020 Is Part Of LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ECOOP.2020.28 urn:nbn:de:0030-drops-131853 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.28 eng https://creativecommons.org/licenses/by/3.0/legalcode