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

• scientific article; zbMATH DE number 1696821
• 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
• scientific article; zbMATH DE number 1614685 (Why is no real title available?)
• scientific article; zbMATH DE number 1696821 (Why is no real title available?)
• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• 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)

• scientific article; zbMATH DE number 1696821 (Why is no real title available?)
• 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)