Verified spilling and translation validation with repair

DOI10.1007/978-3-319-66107-0_27zbMath1484.68044OpenAlexW2748772204MaRDI QIDQ1687761

Julian Rosemann, Sebastian Hack, Sigurd Schneider

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_27

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Coq
• CakeML
• LVC

Cites Work

• A formally verified compiler back-end
• A Linear First-Order Functional Intermediate Language for Verified Compilers
• Formal Verification of Coalescing Graph-Coloring Register Allocation

This page was built for publication: Verified spilling and translation validation with repair