Certification of Compiler Optimizations Using Kleene Algebra with Tests. - Dexter Kozen; Maria-Christina Patron (Computational Logic, 2000)