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 JulDisplayed time zone: Belfast change
15:40 - 17:00 | |||
15:40 20mResearch paper | Static Analysis for Asynchronous JavaScript Programs Research Papers Thodoris Sotiropoulos Athens University of Economics and Business, Ben Livshits Imperial College London, UK DOI | ||
16:00 20mResearch paper | A Program Logic for First-Order Encapsulated WebAssembly Research Papers Conrad Watt University of Cambridge, Petar Maksimović Imperial College London, UK and Mathematical Institute of the Serbian Academy of Sciences and Arts, Serbia, Neel Krishnaswami Computer Laboratory, University of Cambridge, Philippa Gardner Imperial College London DOI Media Attached | ||
16:20 20mResearch paper | Garbage-free Abstract Interpretation through Abstract Reference Counting Research Papers Noah Van Es Sofware Languages Lab, Vrije Universiteit Brussel, Quentin Stiévenart Vrije Universiteit Brussel, Belgium, Coen De Roover Vrije Universiteit Brussel DOI | ||
16:40 20mResearch paper | Eventually Sound Points-To Analysis with Specifications Research Papers Osbert Bastani University of Pennsylvania, Rahul Sharma Microsoft Research, Lazaro Clapp Stanford University, Saswat Anand Stanford University, Alex Aiken Stanford University DOI Media Attached |