HipSpec : Automating Inductive Proofs of Program Properties

We present ongoing work on HipSpec, a system for automaticallyderiving and proving properties about functional programs. HipSpec usesa combination of theory formation, counter example testing andinductive theorem proving to automatically generate a set ofequational theorems about recursive functions in a program, which are laterused as a background theory for proving stated properties about a program.Initial experiments are encouraging; our initial HipSpec prototype already performs comparably to other, similar systems, even being able to deal with some properties other systems cannot handle.