A Self-certifying Compilation Framework for WebAssembly
| Autor: | Kedar S. Namjoshi, Anton Xue |
|---|---|
| Rok vydání: | 2021 |
| Předmět: |
050101 languages & linguistics
Intermediate language Computer science Programming language 05 social sciences Correctness proofs 02 engineering and technology computer.software_genre Mathematical proof Outcome (game theory) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Validator 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Compiler computer |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030670665 VMCAI |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|