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

Funding

Fragoso Santos, Gardner, and Maksimović were partially supported by the EPSRC Programme Grant "REMS: Rigorous Engineering for Mainstream Systems" (EP/K008528/1) and the EPSRC Fellowship "VetSpec: Verified Trustworthy Software Specification" (EP/R034567/1). Fragoso Santos was partially supported by national funds through Fundação para a Ciência e a Tecnologia (FCT), with reference UIDB 2020 (INESC-ID multi-annual funding). Sampaio was supported by a CAPES Foundation Scholarship, process number 88881.129599/2016-01.

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
    0
    Metadata Views

Related Article

  • Gabriela Sampaio, José Fragoso Santos, Petar Maksimović, and Philippa Gardner, "A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications", in 34th European Conference on Object-Oriented Programming (ECOOP 2020), LIPIcs, Vol. 166, pp. 28:1 - 28:29, 2020. https://doi.org/10.4230/LIPIcs.ECOOP.2020.28

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact