Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra

DOI10.1007/978-3-642-17796-5_2MaRDI QIDQ3067464zbMATH OpenOpenAlexFDO

Authors Claude Bolduc, Béchir Ktari

Publication date 21 January 2011

Published in Algebraic Methodology and Software Technology (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Recommendations

• Certification of compiler optimizations using Kleene algebra with tests
• Visibly pushdown Kleene algebra and its use in interprocedural analysis of (mutually) recursive programs
• Verification of the correctness of compiler optimization using co-induction
• Relational Methods in Computer Science
• Specification, verification and prototyping of an optimized compiler

Cites work

• A completeness theorem for Kleene algebras and the algebra of regular events
• Certification of compiler optimizations using Kleene algebra with tests
• Kleene algebra with tests: Completeness and decidability
• Proof generation in the Touchstone theorem prover
• Stack-based typed assembly language
• Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra
• Visibly pushdown Kleene algebra and its use in interprocedural analysis of (mutually) recursive programs
• Visibly pushdown languages

Cited in

(4)

• Certification of compiler optimizations using Kleene algebra with tests
• Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra
• Visibly pushdown Kleene algebra and its use in interprocedural analysis of (mutually) recursive programs
• Verification of the correctness of compiler optimization using co-induction

Describes a project that uses

Uses Software

• TALx86

This page was built for publication: Verification of common interprocedural compiler optimizations using visibly pushdown Kleene algebra

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