Formal Adventures in WebAssembly

Dr Conrad Watt, University of Cambridge
Chaired by
Dr Umang MATHUR, Assistant Professor, School of Computing

24 Nov 2022 Thursday, 03:00 PM to 04:00 PM

MR3, COM2-02-26 and via Zoom (Hybrid)

WebAssembly is the first general-purpose programming language to be introduced natively to the Web since JavaScript. It is the result of a rare collaboration between a number of major tech companies, and is designed to be a "compilation target for the Web", allowing programs written in a variety of languages to be executed directly in Web pages.

Uniquely, WebAssembly's normative specification is stated in terms of a fully formal semantics. This represents an unprecedented opportunity for programming language researchers to practice their craft while maintaining a close association with the language's official development process.

This talk will give an overview of my recent efforts to make good on this opportunity. I will discuss my mechanisations of WebAssembly's semantics in Isabelle and Coq, which have been used not only to find and correct errors on the official specification, but also to verify a fuzzing oracle which is now used in the testing infrastructure of one of WebAssembly's most widely-used implementations. I will also describe my work in standardising WebAssembly's concurrency extension, in particular the language's relaxed memory model.

Conrad Watt is a Research Fellow at Peterhouse, University of Cambridge. He currently serves as a Co-Chair of the WebAssembly Community Group, the main standards body for the language; and as an Invited Expert to the W3C's administrative WebAssembly Working Group.