@inproceedings{kozen2000certification,
 title = {Certification of Compiler Optimizations Using {Kleene} Algebra with Tests},
 author = {Kozen, Dexter and Patron, Maria-Cristina},
 year = {2000},
 booktitle = {Computational Logic — CL 2000},
 pages = {568--582},
 organization = {Springer},
 series = {Lecture Notes in Computer Science},
 volume = {1861},
 doi = {10.1007/3-540-44957-4_38}
}