A Framework for Formal Verification of Compiler Optimizations

DOI10.1007/978-3-642-14052-5_26MaRDI QIDQ5747662zbMATH OpenOpenAlexFDO

Authors William Mansky, Elsa Gunter

Publication date 14 September 2010

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-14052-5_26

zbMATH Keywords

optimizing compilersprogram transformationstemporal logictheorem proving

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 512903
• Types for Proofs and Programs
• Specification, verification and prototyping of an optimized compiler
• Verification of the correctness of compiler optimization using co-induction
• Generating compiler optimizations from proofs
• Compositional verification of compiler optimisations on relaxed memory
• scientific article; zbMATH DE number 1418459

Cited in

(22)

• Compiler optimization correctness by temporal logic
• A formal semantics of the GraalVM intermediate representation
• A formally verified compiler back-end
• scientific article; zbMATH DE number 1670745 (Why is no real title available?)
• scientific article; zbMATH DE number 1696821 (Why is no real title available?)
• Weakest precondition synthesis for compiler optimizations
• Formalizing the LLVM intermediate representation for verified program transformations
• Formal verification of translation validators
• scientific article; zbMATH DE number 512903 (Why is no real title available?)
• scientific article; zbMATH DE number 1948401 (Why is no real title available?)
• Mechanized verification of computing dominators for formalizing compilers
• From Verification to Optimizations
• Proving correctness of compiler optimizations by temporal logic
• Verifying optimizations for concurrent programs
• Generating compiler optimizations from proofs
• Automated soundness proofs for dataflow analyses and transformations via local rules
• A verifiable SSA program representation for aggressive compiler optimization
• Formal verification of object layout for C++ multiple inheritance
• Verification of the correctness of compiler optimization using co-induction
• Types for Proofs and Programs
• Icing: supporting fast-math style optimizations in a verified compiler
• Formal compiler construction in a logical framework

This page was built for publication: A Framework for Formal Verification of Compiler Optimizations

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