Certification of Compiler Optimizations Using Kleene Algebra with Tests kozen2000certificationComputational Logic — CL 2000 · 2000