Open Collections

Abstract

Data structures such as lists and arrays are commonly used in real programs to store and manipulate data. To verify such programs, a verification language needs to provide a representation of data structures and tools to reason about them. The Viper verification language enables users to model recursive data structures using predicates and random-access data structures using quantified permissions. While Viper supports heap-dependent functions to express aggregate properties on recursive data structures, it cannot express the same properties for random-access data structures without involving recursion. We introduce a novel technique to support reasoning about aggregate properties on random-access data structures; we call such properties heap-dependent folds. We provide an encoding of this technique using the built-in constructs of Viper, allowing the verifier to prove fold-like properties without recursion or induction. Finally, we implement our design into a Viper plugin. The plugin introduces a new syntax for expressing folds on user-defined data structures and automatically generates relevant axioms to automate proofs.