A Self-Certifying Compilation Framework for WebAssembly
A self-certifying compiler is designed to generate a correctness proof for each optimization performed during compilation. The generated proofs are checked automatically by an independent proof validator. The outcome is formally verified compilation, achieved without formally verifying the compiler. This paper describes the design and implementation of a self-certifying compilation framework for WebAssembly, a new intermediate language supported by all major browsers.
Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 18:30
|Proving the existence of fair paths in infinite state systems|
Enrico Magnago Fondazione Bruno Kessler, Alberto Griggio Fondazione Bruno Kessler, Alessandro Cimatti Fondazione Bruno KesslerMedia Attached
|A Self-Certifying Compilation Framework for WebAssembly|