Certification of compiler optimizations using Kleene algebra with tests

DOI10.1007/3-540-44957-4_38MaRDI QIDQ2767087zbMATH OpenFDO

Authors Dexter Kozen, Maria-Cristina Patron

Publication date 28 January 2002

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-44957-4_38

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of compilers and interpreters (68N20) Formal languages and automata (68Q45)

Recommendations

• Verification of the correctness of compiler optimization using co-induction
• Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra
• A Framework for Formal Verification of Compiler Optimizations
• Kleene algebra with tests and Coq tools for while programs
• Compiler optimization correctness by temporal logic

Cited in

(30)

• Specification, verification and prototyping of an optimized compiler
• Compiler optimization correctness by temporal logic
• On tools for completeness of Kleene algebra with hypotheses
• Weakest precondition synthesis for compiler optimizations
• Canonical finite models of Kleene algebra with tests
• Equality saturation: a new approach to optimization
• Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra
• Algebraic_VCs
• scientific article; zbMATH DE number 1948401 (Why is no real title available?)
• Completeness for identity-free Kleene lattices
• Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)
• Generating compiler optimizations from proofs
• Verification of the correctness of compiler optimization using co-induction
• Algebraic separation logic
• Kleene algebra with observations
• Completeness and the finite model property for Kleene algebra, reconsidered
• A complete inference system for skip-free guarded Kleene algebra with tests
• On tools for completeness of Kleene algebra with hypotheses
• On the complexity of reasoning in Kleene algebra with commutativity conditions
• Completeness theorems for Kleene algebra with tests and top
• An elementary proof of the FMP for Kleene algebra
• Correctly compiling proofs about programs without proving compilers correct
• On propositional program equivalence (extended abstract)
• Paraconsistent relations as a variant of Kleene algebras
• A completeness theorem for probabilistic regular expressions
• Well-behaved (co)algebraic semantics of regular expressions in Dafny
• Synchronous Kleene algebra
• A Kleene algebra with tests for union bound reasoning about probabilistic programs
• Building program construction and verification tools from algebraic principles
• Abstract abstract reduction

This page was built for publication: Certification of compiler optimizations using Kleene algebra with tests

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