DROPS

Document

Utilising and Scaling the WebAssembly Semantics (Dagstuhl Seminar 25241)

Authors: Amal Ahmed, Andreas Rossberg, Deian Stefan, Conrad Watt, and Michelle Thalakottur

Published in: Dagstuhl Reports, Volume 15, Issue 6 (2026)

Abstract

WebAssembly (Wasm) is a safe and portable, low level bytecode format used in browsers, IoT applications, cloud, edge, embedded systems and blockchains. Its popularity as a technology for both practically building and theoretically investigating verified and secure systems has been growing rapidly. This Dagstuhl Seminar brought together leading academics and industry representatives involved in Wasm, both as designers, implementers or clients of the technology, to exchange ideas around topics such as tools for formal specification, verified compilation, software fault isolation and language interoperability.

Cite as

Amal Ahmed, Andreas Rossberg, Deian Stefan, Conrad Watt, and Michelle Thalakottur. Utilising and Scaling the WebAssembly Semantics (Dagstuhl Seminar 25241). In Dagstuhl Reports, Volume 15, Issue 6, pp. 51-68, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{ahmed_et_al:DagRep.15.6.51,
  author =	{Ahmed, Amal and Rossberg, Andreas and Stefan, Deian and Watt, Conrad and Thalakottur, Michelle},
  title =	{{Utilising and Scaling the WebAssembly Semantics (Dagstuhl Seminar 25241)}},
  pages =	{51--68},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2026},
  volume =	{15},
  number =	{6},
  editor =	{Ahmed, Amal and Rossberg, Andreas and Stefan, Deian and Watt, Conrad and Thalakottur, Michelle},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.6.51},
  URN =		{urn:nbn:de:0030-drops-255770},
  doi =		{10.4230/DagRep.15.6.51},
  annote =	{Keywords: Compilers, Formal Methods, JavaScript, Proof Assistants, Runtimes, Software Verification, Webassembly}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2019.9

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}
}

Search Results

Documents authored by Watt, Conrad

Utilising and Scaling the WebAssembly Semantics (Dagstuhl Seminar 25241)

Abstract

Cite as

A Program Logic for First-Order Encapsulated WebAssembly

Abstract

Cite as

Thanks for your feedback!

Could not send message