Automatic Reasoning on Recursive Data-Structures with Sharing
Abstract
We consider the problem of automatically verifying programs which manipulate arbitrary data structures. Our specification language is expressive, contains a notion of \emph{separation}, and thus enables a precise specification of \emph{frames}. The main contribution then is a program verification method which combines strongest postcondition reasoning in the form symbolic execution, unfolding recursive definitions of the data structure in question, and a new frame rule to achieve \emph{local reasoning} so that proofs can be compositional. Finally, we present an implementation of our verifier, and demonstrate automation on a number of representative programs. In particular, we present the first automatic proof of a classic graph marking algorithm, paving the way for dealing with a class of programs which traverse a complex data structure.
Cite
@article{arxiv.1511.07267,
title = {Automatic Reasoning on Recursive Data-Structures with Sharing},
author = {Duc-Hiep Chu and Joxan Jaffar},
journal= {arXiv preprint arXiv:1511.07267},
year = {2017}
}
Comments
13 pages