View article

It has often been claimed that model checking, special purpose automated deduction or interactive theorem proving are needed for formal program development. We demonstrate that off-the-shelf automated proof and counterexample search is an interesting alternative if combined with the right domain model. We implement variants of Kleene algebras axiomatically in Prover9/Mace4 and perform proof experiments about Hoare, dynamic, temporal logics, concurrency control and termination analysis. They confirm that a simple automated analysis of some important program properties is possible. Particular benefits of this approach include “soft” model checking in a first-order setting, cross-theory reasoning between standard formalisms and full automation of some (co)inductive arguments. Kleene algebras might therefore provide light-weight formal methods with heavy-weight automation.