Open Collections

Tokaeo, Peeranat

University of British Columbia

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.

Text

2024-01-10

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/87193

Computer Science

University of British Columbia

UBCV

http://creativecommons.org/licenses/by-nc-nd/4.0/