Document Open Access Logo

A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact)

Authors Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, Philippa Gardner



PDF
Thumbnail PDF

Artifact Description

DARTS.6.2.5.pdf
  • Filesize: 360 kB
  • 3 pages

Document Identifiers

Author Details

Gabriela Sampaio
  • Imperial College London, United Kingdom
José Fragoso Santos
  • INESC-ID/Instituto Superior Técnico, Universidade de Lisboa, Portugal
  • Imperial College London, United Kingdom
Petar Maksimović
  • Imperial College London, United Kingdom
Philippa Gardner
  • Imperial College London, United Kingdom

Cite AsGet BibTex

Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner. A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 5:1-5:3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/DARTS.6.2.5

Artifact

Abstract

This artifact contains the implementation of JaVerT.Click, a symbolic analysis tool for modern event-driven Web applications. The tool extends JaVerT 2.0, a state-of-the-art symbolic execution tool for JavaScript (JS), with JS 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 mostly follow the respective standards line-by-line and are all thoroughly tested against the official test suite. We also evaluate JaVerT.Click by performing symbolic analysis on two real-world libraries: cash and p-map, finding three previously unknown bugs.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Software and its engineering → Software testing and debugging
Keywords
  • Events
  • DOM
  • JavaScript
  • promises
  • symbolic execution
  • bug-finding

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. J. Fragoso Santos, P. Maksimović, G. Sampaio, and P. Gardner. JaVerT 2.0: Compositional Symbolic Execution for JavaScript. PACMPL, 3(POPL):66, 2019. Google Scholar
  2. S. Sorhus. p-map (GitHub). https://github.com/sindresorhus/p-map, visited 05/2020.
  3. K. Wheeler, S. Shaw, and F. Spampinato. cash (GitHub). https://github.com/kenwheeler/cash, visited 05/2020.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail