HipSpec : Automating Inductive Proofs of Program Properties
Koen Claessen, Moa Johansson, Dan Rosén, Nick Smallbone · EPiC series in computing · 2018
We present ongoing work on HipSpec, a system for automatically deriving and proving properties about functional programs. HipSpec uses a combination of theory formation, counter example testing and inductive theorem proving to automatically generate a set of equational theorems about recursive functions in a program, which are later used 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.