Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution

TL;DR

This paper introduces a novel symbolic execution method that automatically verifies iterated separating conjunctions in permission logics, enabling the analysis of complex data structures like arrays and graphs.

Contribution

It presents the first symbolic execution approach supporting general iterated separating conjunctions with a new heap representation and quantifier management, integrated into the Viper verifier.

Findings

Supports verification of unbounded heap sets

Maintains predictable and efficient SMT performance

Compatible with fractional permissions and recursive predicates

Abstract

In permission logics such as separation logic, the iterated separating conjunction is a quantifier denoting access permission to an unbounded set of heap locations. In contrast to recursive predicates, iterated separating conjunctions do not prescribe a structure on the locations they range over, and so do not restrict how to traverse and modify these locations. This flexibility is important for the verification of random-access data structures such as arrays and data structures that can be traversed in multiple ways such as graphs. Despite its usefulness, no automatic program verifier natively supports iterated separating conjunctions; they are especially difficult to incorporate into symbolic execution engines, the prevalent technique for building verifiers for these logics. In this paper, we present the first symbolic execution technique to support general iterated separating conjunctions. We propose a novel representation of symbolic heaps and flexible support for logical specifications that quantify over heap locations. Our technique exhibits predictable and fast performance despite employing quantifiers at the SMT level, by carefully controlling quantifier instantiations. It is compatible with other features of permission logics such as fractional permissions, recursive predicates, and abstraction functions. Our technique is implemented as an extension of the Viper verification infrastructure.