POPL 2021 (series) / VMCAI 2021 (series) / VMCAI 2021 - 22nd International Conference on Verification, Model Checking, and Abstract Interpretation /
A Self-Certifying Compilation Framework for WebAssembly
Sun 17 Jan 2021 18:15 - 18:30 at VMCAI - Infinite-State Systems and Compilation Chair(s): Orna Grumberg
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
Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 18:30 | Infinite-State Systems and CompilationVMCAI at VMCAI Chair(s): Orna Grumberg Technion – Israel Institute of Technology | ||
18:00 15mTalk | Proving the existence of fair paths in infinite state systems VMCAI Enrico Magnago Fondazione Bruno Kessler, Alberto Griggio Fondazione Bruno Kessler, Alessandro Cimatti Fondazione Bruno Kessler Media Attached | ||
18:15 15mTalk | A Self-Certifying Compilation Framework for WebAssembly VMCAI Media Attached |