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 12 articles )
Showing results 1 to 12 of 12.
- Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
- Drămnesc, Isabela; Jebelean, Tudor; Stratulat, Sorin: Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques (2019)
- Demba, Moussa: Equivalence checking of two functional programs using inductive theorem provers (2018)
- Cruanes, Simon: Superposition with structural induction (2017)
- Smallbone, Nicholas; Johansson, Moa; Claessen, Koen; Algehed, Maximilian: Quick specifications for the busy programmer (2017)
- 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)