Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
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 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:00 - 18:30: Infinite-State Systems and CompilationVMCAI at VMCAI
Chair(s): Orna GrumbergTechnion – Israel Institute of Technology
18:00 - 18:15
Talk
Proving the existence of fair paths in infinite state systems
VMCAI
Enrico MagnagoFondazione Bruno Kessler, Alberto GriggioFondazione Bruno Kessler, Alessandro CimattiFondazione Bruno Kessler
Media Attached
18:15 - 18:30
Talk
A Self-Certifying Compilation Framework for WebAssembly
VMCAI
Kedar NamjoshiNokia Bell Labs, Anton XueUniversity of Pennsylvania
Media Attached