Computing Publications

Publications Home » Zeno: A tool for the automatic ve...

Zeno: A tool for the automatic verification of algebraic properties of functional programs

William Sonnex, Sophia Drossopoulou, Susan Eisenbach

Technical Report
February, 2011
Abstract

Most functional programs rely heavily on recursively defined structures and pattern matching thereupon. Proving properties of such programs often requires a proof by induction, which many theorem provers have difficulty addressing.

In this paper we present Zeno, a new tool for the automatic verification of simple properties of functional programs. We define a minimal functional language along with a subset of first order logic in which to express properties to be proven. Zeno constructs a proof tree by iteratively reducing the goal into an equivalent conjunction of several simpler sub-goals, terminating when all leaves are trivially true. Building this tree requires the exploration of many alternatives and we give sophisticated techniques for the reduction of this search space through the analysis of function definitions.

We provide a comparison with the rippling based tool IsaPlanner and the industrial strength tool ACL2s. Using a test suite from the IsaPlanner website we found that Zeno could prove strictly more properties than either, and in as good times.

PDF of full publication (295 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.