Automating Proofs of Data-Structure Properties in Imperative Programs

TL;DR

This paper introduces an advanced automated proof method for reasoning about data structures in imperative programs, overcoming limitations of existing unfold-and-match approaches by incorporating induction hypotheses for more effective verification.

Contribution

The authors present a novel proof technique that extends current methods with automatic formula rewriting and induction hypotheses, enabling systematic reasoning about complex program obligations.

Findings

Successfully verified common data structure lemmas

Eliminated the need for user-provided lemmas in benchmarks

Enhanced verification efficiency by reducing search space

Abstract

We consider the problem of automated reasoning about dynamically manipulated data structures. The state-of-the-art methods are limited to the unfold-and-match (U+M) paradigm, where predicates are transformed via (un)folding operations induced from their definitions before being treated as uninterpreted. However, proof obligations from verifying programs with iterative loops and multiple function calls often do not succumb to this paradigm. Our contribution is a proof method which -- beyond U+M -- performs automatic formula re-writing by treating previously encountered obligations in each proof path as possible induction hypotheses. This enables us, for the first time, to systematically reason about a wide range of obligations, arising from practical program verification. We demonstrate the power of our proof rules on commonly used lemmas, thereby close the remaining gaps in existing state-of-the-art systems. Another impact, probably more important, is that our method regains the power of compositional reasoning, and shows that the usage of user-provided lemmas is no longer needed for the existing set of benchmarks. This not only removes the burden of coming up with the appropriate lemmas, but also significantly boosts up the verification process, since lemma applications, coupled with unfolding, often induce very large search space.