Wed 17 Jul 2019 16:00 - 16:20 at Mancy - Program Analysis 1 Chair(s): Yannis Smaragdakis

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.

Wed 17 Jul

ecoop-2019-papers
15:40 - 17:00: Research Papers - Program Analysis 1 at Mancy
Chair(s): Yannis SmaragdakisUniversity of Athens
ecoop-2019-papers15:40 - 16:00
Research paper
Thodoris SotiropoulosAthens University of Economics and Business, Ben LivshitsImperial College London, UK
DOI
ecoop-2019-papers16:00 - 16:20
Research paper
Conrad WattUniversity of Cambridge, Petar MaksimovićImperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Neel KrishnaswamiComputer Laboratory, University of Cambridge, Philippa GardnerImperial College London
DOI
ecoop-2019-papers16:20 - 16:40
Research paper
Noah Van EsSofware Languages Lab, Vrije Universiteit Brussel, Quentin StiévenartVrije Universiteit Brussel, Belgium, Coen De RooverVrije Universiteit Brussel
DOI
ecoop-2019-papers16:40 - 17:00
Research paper
Osbert BastaniUniversity of Pennsylvania, Rahul SharmaMicrosoft Research, Lazaro ClappStanford University, Saswat AnandStanford University, Alex AikenStanford University
DOI