@article{kozen1997kleene,
 title = {Kleene Algebra with Tests},
 author = {Kozen, Dexter},
 year = {1997},
 month = may,
 doi = {10.1145/256167.256195},
 url = {https://dl.acm.org/doi/10.1145/256167.256195},
 journal = {ACM Transactions on Programming Languages and Systems},
 volume = {19},
 number = {3},
 pages = {427--443},
 issn = {0164-0925},
 publisher = {ACM},
 abstract = {We introduce Kleene algebra with tests, an equational system for manipulating programs. We give a purely equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with tests and commutativity conditions in program equivalence proofs.}
}