Automating inductive proofs using theory exploration 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.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Demba, Moussa: Equivalence checking of two functional programs using inductive theorem provers (2018)
- Brotherston, James; Gorogiannis, Nikos: Disproving inductive entailments in separation logic via base pair approximation (2015)
- Claessen, Koen; Johansson, Moa; Rosén, Dan; Smallbone, Nicholas: TIP: tons of inductive problems (2015)
- Eberhard, Sebastian; Hetzl, Stefan: Inductive theorem proving based on tree grammars (2015)
- Grechanik, S.A.: Proving properties of functional programs by equality saturation (2015)
- Rosén, Dan; Smallbone, Nicholas: TIP: tools for inductive provers (2015)
- Johansson, Moa; Rosén, Dan; Smallbone, Nicholas; Claessen, Koen: Hipster: integrating theory exploration in a proof assistant (2014)
- Claessen, Koen; Johansson, Moa; Rosén, Dan; Smallbone, Nicholas: Automating inductive proofs using theory exploration (2013)