Compiler optimization correctness by temporal logic

DOI10.1023/B:LISP.0000029444.99264.C0MaRDI QIDQ1768477zbMATH OpenWikidataFDO

Authors David Lacey, Neil D. Jones, Eric Van Wyk, Carl Christian Frederiksen

Publication date 15 March 2005

Published in Higher-Order and Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

model checkingtemporal logicoptimizing compilerscompiler verification

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Recommendations

• Proving correctness of compiler optimizations by temporal logic
• A Framework for Formal Verification of Compiler Optimizations
• scientific article; zbMATH DE number 1693488
• scientific article; zbMATH DE number 1696821
• Types for Proofs and Programs

Cited in

(15)

• scientific article; zbMATH DE number 1948401 (Why is no real title available?)
• Proving correctness of compiler optimizations by temporal logic
• A higher-order strategy for eliminating common subexpressions
• scientific article; zbMATH DE number 1696821 (Why is no real title available?)
• Types for Proofs and Programs
• Securing a compiler transformation
• Program and proof optimizations with type systems
• Equality saturation: a new approach to optimization
• Simple relational correctness proofs for static analyses and program transformations
• Extracting program logics from abstract interpretations defined by logical relations
• Generating compiler optimizations from proofs
• Specifications can make programs run faster
• Weakest precondition synthesis for compiler optimizations
• Asymptotic speedups, bisimulation and distillation (work in progress)
• scientific article; zbMATH DE number 1693488 (Why is no real title available?)

This page was built for publication: Compiler optimization correctness by temporal logic

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