Proof Automation in Kleene Algebra

in W. Dosch, C. Grelck, A. Stümpel (eds.): 14. Kolloquium Programmiersprachen unf Grundlagen der Programmierung, Technical Report, Institutes for Computer Science and Mathematics, University of Lübeck, pp. 87-92, September 2007

Abstract: It has often been claimed that model checking, special purpose automated deduction or interactive theorem proving are needed for formal program development. Recently, it has been demonstrated that off-the-shelf automated proof and counterexample search is an interesting alternative if combined with the right domain model. Furthermore it has been shown that variants of Kleene algebra might provide ligh t-weight formal methods with heavy-weight automation.
In this paper we give a brief overview of a number of program analysis and computer mathematics tasks where (variants of) Kleene algebra combined with automated theorem provers are already applied.

Downloads:

• A-07-07_pp87-92  -  (proof_automation_in_Kleene_algebra.pdf, 125 KB)