Imperial College London
Alternate

Emeritus ProfessorSusanEisenbach

Faculty of Engineering, Department of Computing

Emeritus Professor of Computing
 
 
 
//

Contact

 

s.eisenbach Website

 
 
//

Location

 

Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Sonnex:2012:10.1007/978-3-642-28756-5_28,
author = {Sonnex, W and Drossopoulou, S and Eisenbach, S},
doi = {10.1007/978-3-642-28756-5_28},
pages = {407--421},
publisher = {Springer Berlin Heidelberg},
title = {Zeno: An automated prover for properties of recursive data structures},
url = {http://dx.doi.org/10.1007/978-3-642-28756-5_28},
year = {2012}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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.
AU  - Sonnex,W
AU  - Drossopoulou,S
AU  - Eisenbach,S
DO  - 10.1007/978-3-642-28756-5_28
EP  - 421
PB  - Springer Berlin Heidelberg
PY  - 2012///
SN  - 0302-9743
SP  - 407
TI  - Zeno: An automated prover for properties of recursive data structures
UR  - http://dx.doi.org/10.1007/978-3-642-28756-5_28
UR  - http://www.haskell.org/haskellwiki/Zeno
ER  -
Download