Zeno: an automated prover for properties of recursive data structures Zeno is a new tool for the automatic generation of proofs of simple properties of functions over recursively defined data structures. It takes a Haskell program and an assertion as its goal and tries to contruct a proof for that goal. If successful, it converts the proof into Isabelle code. Zeno searches for a proof tree by iteratively reducing the goal into a conjunction of sub-goals, terminating when all leaves are proven true.par This process requires the exploration of many alternatives. We have adapted known, and developed new, heuristics for the reduction of the search space. Our new heuristics aim to promote the application of function definitions, and avoid the repetition of similar proof steps.par We compare with the rippling based tool IsaPlanner and the industrial strength tool ACL2s on the basis of a test suite from the IsaPlanner website. We found that Zeno compared favourably with these tools both in terms of theorem proving power and speed.
References in zbMATH (referenced in 9 articles , 1 standard article )
Showing results 1 to 9 of 9.
- Johansson, Moa: Lemma discovery for induction. A survey (2019)
- Reger, Giles; Voronkov, Andrei: Induction in saturation-based proof search (2019)
- 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)
- Claessen, Koen; Johansson, Moa; Rosén, Dan; Smallbone, Nicholas: Automating inductive proofs using theory exploration (2013)
- Leino, K. Rustan M.: Automating induction with an SMT solver (2012)
- Sonnex, William; Drossopoulou, Sophia; Eisenbach, Susan: Zeno: an automated prover for properties of recursive data structures (2012)