Automated Reasoning in Kleene Algebra

12 years 12 months ago
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.
Georg Struth, Peter Höfner
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2007
Where CADE
Authors Georg Struth, Peter Höfner
Comments (0)