Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL.

Alasdair Armstrong, Georg Struth, Tjark Weber

Browse the full ITP paper archive.