 |
    |
Automating Inductive Proofs Using Theory Exploration
Koen Claessen, Moa Johansson, Dan Rosén, and Nicholas Smallbone
Department of Computer Science and Engineering, Chalmers University of Technology, Swedenkoen@chalmers.se
moa.johansson@chalmers.se
danr@chalmers.se
nicsma@chalmers.se
Abstract. HipSpec is a system for automatically deriving and proving properties about functional programs. It uses a novel approach, combining theory exploration, counterexample testing and inductive theorem proving. HipSpec automatically generates a set of equational theorems about the available recursive functions of a program. These equational properties make up an algebraic specification for the program and can in addition be used as a background theory for proving additional user-stated properties. Experimental results are encouraging: HipSpec compares favourably to other inductive theorem provers and theory exploration systems.
LNAI 7898, p. 392 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013