Formal verification of coalescing graph-coloring register allocation

DOI10.1007/978-3-642-11957-6_9MaRDI QIDQ3558221zbMATH OpenOpenAlexFDO

Authors Sandrine Blazy, Benoît Robillard, Andrew W. Appel

Publication date 4 May 2010

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-11957-6_9

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Graph theory (including graph drawing) in computer science (68R10)

Recommendations

• Register allocation by proof transformation
• Programming Languages and Systems
• scientific article; zbMATH DE number 1956567
• A linear first-order functional intermediate language for verified compilers
• scientific article; zbMATH DE number 1956454

Cited in

(8)

• Verified spilling and translation validation with repair
• Register allocation by proof transformation
• Proof-producing synthesis of CakeML from monadic HOL functions
• A linear first-order functional intermediate language for verified compilers
• Tool-Based Verification of a Relational Vertex Coloring Program
• A Framework for End-to-End Verification and Evaluation of Register Allocators
• scientific article; zbMATH DE number 1956454 (Why is no real title available?)
• The verified CakeML compiler backend

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Formal verification of coalescing graph-coloring register allocation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3558221)