Automatic Reasoning on Recursive Data-Structures with Sharing

TL;DR

This paper introduces an automated verification method for programs manipulating recursive data structures, combining symbolic execution, recursive unfolding, and a novel frame rule for local reasoning, demonstrated on complex algorithms.

Contribution

It presents a new verification approach that integrates strongest postcondition reasoning with a frame rule for local reasoning, enabling automation on complex recursive data structures.

Findings

Automated proof of a classic graph marking algorithm.

Effective verification of programs with complex data structures.

Implementation demonstrates practical applicability.

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.