Verification of Common Interprocedural Compiler Optimizations Using Visibly Pushdown Kleene Algebra

摘要

Visibly pushdown Kleene algebra is an algebraic system using only propositional reasoning while still being able to represent well-known constructs of programming languages (sequences, alternatives, loops and code blocks) in a natural way. In this paper, this system is used to verify the following interprocedural compiler optimizations: interprocedural dead code elimination, inlining of functions, tail-recursion elimination, procedure reordering and function cloning. The proofs are equational and machine-verifiable.