Mon 8 Jan 2018 13:30 - 14:00 at Museum A - Verified Applications Chair(s): K. Rustan M. Leino

<p>WebAssembly is a new low-level language currently being implemented in all major web browsers. It is designed to become the universal compilation target for the web, obsoleting existing solutions in this area, such as asm.js and Native Client. The WebAssembly working group has incorporated formal techniques into the development of the language, but their efforts so far have focussed on pen and paper formal specification.</p>

<p>We present a mechanised Isabelle specification for the WebAssembly language, together with a verified executable interpreter and type checker. Moreover, we present a fully mechanised proof of the soundness of the WebAssembly type system, and detail how our work on this proof has exposed several issues with the official WebAssembly specification, influencing its development. Finally, we give a brief account of our efforts in performing differential fuzzing of our interpreter against industry implementations.</p>

Mon 8 Jan

Displayed time zone: Tijuana, Baja California change

13:30 - 15:30
Verified ApplicationsCPP at Museum A
Chair(s): K. Rustan M. Leino Amazon
13:30
30m
Talk
Mechanising and Verifying the WebAssembly Specification
CPP
Conrad Watt University of Cambridge, UK
DOI
14:00
30m
Talk
Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
CPP
Sidney Amani UNSW, Australia, Myriam Bégel ENS Paris-Saclay, France, Maksym Bortin , Mark Staples CSIRO, Australia
DOI
14:30
30m
Talk
Mechanising Blockchain Consensus
CPP
George Pîrlea University College London, Ilya Sergey University College London
DOI Pre-print
15:00
30m
Talk
Formal Microeconomic Foundations and the First Welfare Theorem
CPP
Cezary Kaliszyk University of Innsbruck, Julian Parsert University of Innsbruck, Austria