Commit f95c7f85 authored by Teresa Carbajo-Garcia's avatar Teresa Carbajo-Garcia
Browse files

Update publications.bib

parent 1883b66e
......@@ -1689,8 +1689,32 @@ based on separation logic. We apply our approach to JavaScript,
providing support for full verification, whole-program symbolic
testing, and automatic compositional testing based on bi-abduction.},
author = {Conrad Watt and
Petar Maksimovic and
Neelakantan R. Krishnaswami and
Philippa Gardner },
title = {A Program Logic for First-Order Encapsulated WebAssembly},
booktitle = {Proceedings of the 33 \textsuperscript{rd} European Conference on Object-Oriented Programming (ECOOP’19). },
pages = {10:1–10:30 },
month = jul,
year = {2019},
doi = { 10.4230/LIPIcs.ECOOP.2019.10},
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.},
@Comment{jabref-meta: databaseType:bibtex;}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment