Verification of the correctness of compiler optimization using co-induction

DOI10.1080/09720529.2007.10698123MaRDI QIDQ5421199zbMATH OpenOpenAlexWikidataFDO

Authors M. Thiyagarajan, N. Sairam

Publication date 22 October 2007

Published in Journal of Discrete Mathematical Sciences and Cryptography (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1080/09720529.2007.10698123

zbMATH Keywords

co-algebracompiler optimizationKATmixed automata

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1696821
• Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra
• Specification, verification and prototyping of an optimized compiler
• A Framework for Formal Verification of Compiler Optimizations
• Kleene algebra with tests and Coq tools for while programs

Cites work

• A completeness theorem for Kleene algebras and the algebra of regular events
• A note on Coinduction and Weak Bisimilarity for While Programs
• Derivatives of Regular Expressions
• scientific article; zbMATH DE number 3912289 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 1984270 (Why is no real title available?)

Cited in

(6)

• Specification, verification and prototyping of an optimized compiler
• scientific article; zbMATH DE number 1696821 (Why is no real title available?)
• Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra
• Proving correctness of compiler optimizations by temporal logic
• A Framework for Formal Verification of Compiler Optimizations
• Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves

This page was built for publication: Verification of the correctness of compiler optimization using co-induction

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