When reasoning about functional programs, we often need induction to prove properties about recursive functions. Automating inductive proofs is tricky, not least because they often need auxilliary lemmas which themselves need to be proved by induction.

We solve this by using a method called theory exploration to automatically conjecture interesting properties about a mathematical theory, using testing. The conjectures are then passed on to an automated inductive theorem prover and can, after proof, be used as lemmas when proving other conjectures.

We have implemented this in two state-of-the-art inductive theorem provers: HipSpec (for reasoning about Haskell programs) and Hipster (for the proof-assistant Isabelle/HOL). These systems can be used to automatically generate and prove an algebraic specification for a functional program.

Both HipSpec and Hipster share the same theory exploration component: a system also developed at Chalmers, called QuickSpec. As well as being used for lemma generation for induction, QuickSpec may also be used independently as a light-weight verification tool, interleaving conjecture generation, testing and pruning of uniteresting facts to quickly produce a small candidate specification for a program.