Publications Home » Zeno: An automated prover for pro...
Zeno: An automated prover for properties of recursive data structures
William Sonnex, Sophia Drossopoulou, Susan Eisenbach
- Conference or Workshop Paper
- TACAS
- March, 2012
- Lecture Notes in Computer Science
- Abstract
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.
This process requires the exploration of many alternatives. We have adapted knowand 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.
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.
PDF of full publication (352 kilobytes)- (need help viewing PDF files?)
BibTEX file for the publication - N.B.
- Conditions for downloading publications from this site.
pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.