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 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 18:30
|Proving the existence of fair paths in infinite state systems|
Enrico MagnagoFondazione Bruno Kessler, Alberto GriggioFondazione Bruno Kessler, Alessandro CimattiFondazione Bruno KesslerMedia Attached
|A Self-Certifying Compilation Framework for WebAssembly|