Automated Reasoning in Kleene Algebra

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 light-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 is already applied.

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Georg Struth, Peter Höfner
• Keywords: Automated Reasoning, CADE 2007, Interactive Theorem Proving, Light-weight Formal Methods, Right Domain Model