Portal de Periódicos da CAPES

A Self-certifying Compilation Framework for WebAssembly

2021; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-030-67067-2_7

1611-3349

Kedar S. Namjoshi, Anton Xue,

Parallel Computing and Optimization Techniques

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.