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.
展开▼
