A self-certifying compilation framework for WebAssembly

DOI10.1007/978-3-030-67067-2_7zbMath1472.68032OpenAlexW3119305140MaRDI QIDQ2234063

Kedar S. Namjoshi, Anton Xue

Publication date: 18 October 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-67067-2_7

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (1)

WebAssembly

Uses Software

• TVOC
• z3
• CompCert
• CVT
• SymDiff
• Crellvm
• Loopy

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Translation and run-time validation of loop transformations
• The code validation tool (CVT). Automatic verification of a compilation process
• Regression verification for unbalanced recursive functions
• Validating LR(1) Parsers
• Simple relational correctness proofs for static analyses and program transformations
• Automated Discovery of Simulation Between Programs
• Designing programs that check their work
• From Verification to Optimizations
• Formal certification of a compiler back-end or
• Computer Aided Verification

This page was built for publication: A self-certifying compilation framework for WebAssembly