4 Search Results for "Sampaio, Gabriela"


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

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

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)


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.

Cite as

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)


Copy BibTex To Clipboard

@Article{sampaio_et_al:DARTS.6.2.5,
  author =	{Sampaio, Gabriela and Fragoso Santos, Jos\'{e} and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications (Artifact)}},
  pages =	{5:1--5:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Sampaio, Gabriela and Fragoso Santos, Jos\'{e} and Maksimovi\'{c}, Petar and Gardner, Philippa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.6.2.5},
  URN =		{urn:nbn:de:0030-drops-132028},
  doi =		{10.4230/DARTS.6.2.5},
  annote =	{Keywords: Events, DOM, JavaScript, promises, symbolic execution, bug-finding}
}
Document
A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications

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

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)


Abstract
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.

Cite as

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 28:1-28:29, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{sampaio_et_al:LIPIcs.ECOOP.2020.28,
  author =	{Sampaio, Gabriela and Fragoso Santos, Jos\'{e} and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{A Trusted Infrastructure for Symbolic Analysis of Event-Driven Web Applications}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{28:1--28:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.28},
  URN =		{urn:nbn:de:0030-drops-131853},
  doi =		{10.4230/LIPIcs.ECOOP.2020.28},
  annote =	{Keywords: Events, DOM, JavaScript, promises, symbolic execution, bug-finding}
}
Document
Human-Centric Program Synthesis

Authors: Will Crichton

Published in: OASIcs, Volume 76, 10th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU 2019)


Abstract
Program synthesis techniques offer significant new capabilities in searching for programs that satisfy high-level specifications. While synthesis has been thoroughly explored for input/output pair specifications (programming-by-example), this paper asks: what does program synthesis look like beyond examples? What actual issues in day-to-day development would stand to benefit the most from synthesis? How can a human-centric perspective inform the exploration of alternative specification languages for synthesis? I sketch a human-centric vision for program synthesis where programmers explore and learn languages and APIs aided by a synthesis tool.

Cite as

Will Crichton. Human-Centric Program Synthesis. In 10th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU 2019). Open Access Series in Informatics (OASIcs), Volume 76, pp. 5:1-5:5, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{crichton:OASIcs.PLATEAU.2019.5,
  author =	{Crichton, Will},
  title =	{{Human-Centric Program Synthesis}},
  booktitle =	{10th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU 2019)},
  pages =	{5:1--5:5},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-135-1},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{76},
  editor =	{Chasins, Sarah and Glassman, Elena L. and Sunshine, Joshua},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.PLATEAU.2019.5},
  URN =		{urn:nbn:de:0030-drops-119590},
  doi =		{10.4230/OASIcs.PLATEAU.2019.5},
  annote =	{Keywords: Program synthesis, programming by example, PL/HCI}
}
Document
A Program Logic for First-Order Encapsulated WebAssembly

Authors: Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami, and Philippa Gardner

Published in: LIPIcs, Volume 134, 33rd European Conference on Object-Oriented Programming (ECOOP 2019)


Abstract
We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We design a novel assertion syntax, tailored to WebAssembly’s stack-based semantics and the strong guarantees given by WebAssembly’s type system, and show how to adapt the standard separation logic triple and proof rules in a principled way to capture WebAssembly’s uncommon structured control flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, giving abstract specifications independent of the underlying implementation. We mechanise Wasm Logic and its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formalise and fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, up to transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the first program logic for WebAssembly, and represents a first step towards the creation of static analysis tools for WebAssembly.

Cite as

Conrad Watt, Petar Maksimović, Neelakantan R. Krishnaswami, and Philippa Gardner. A Program Logic for First-Order Encapsulated WebAssembly. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 9:1-9:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{watt_et_al:LIPIcs.ECOOP.2019.9,
  author =	{Watt, Conrad and Maksimovi\'{c}, Petar and Krishnaswami, Neelakantan R. and Gardner, Philippa},
  title =	{{A Program Logic for First-Order Encapsulated WebAssembly}},
  booktitle =	{33rd European Conference on Object-Oriented Programming (ECOOP 2019)},
  pages =	{9:1--9:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-111-5},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{134},
  editor =	{Donaldson, Alastair F.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2019.9},
  URN =		{urn:nbn:de:0030-drops-108011},
  doi =		{10.4230/LIPIcs.ECOOP.2019.9},
  annote =	{Keywords: WebAssembly, program logic, separation logic, soundness, mechanisation}
}
  • Refine by Author
  • 3 Gardner, Philippa
  • 3 Maksimović, Petar
  • 2 Fragoso Santos, José
  • 2 Sampaio, Gabriela
  • 1 Crichton, Will
  • Show More...

  • Refine by Classification
  • 2 Software and its engineering → Formal software verification
  • 2 Software and its engineering → Software testing and debugging
  • 1 Software and its engineering → Programming by example
  • 1 Theory of computation → Separation logic

  • Refine by Keyword
  • 2 DOM
  • 2 Events
  • 2 JavaScript
  • 2 bug-finding
  • 2 promises
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 3 2020
  • 1 2019

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