2016/03/02 by Péter Müller, Müller, Peter, Malte Schwerhoff +3 · 1 citation
Computer Science · #F.3.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1603.00649
openalex publication_date 2016/03/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In permission logics such as separation logic, the iterated separating\nconjunction is a quantifier denoting access permission to an unbounded set of\nheap locations. In contrast to recursive predicates, iterated separating\nconjunctions do not prescribe a structure on the locations they range over, and\nso do not restrict how to traverse and modify these locations. This flexibility\nis important for the verification of random-access data structures such as\narrays and data structures that can be traversed in multiple ways such as\ngraphs. Despite its usefulness, no automatic program verifier natively supports\niterated separating conjunctions; they are especially difficult to incorporate\ninto symbolic execution engines, the prevalent technique for building verifiers\nfor these logics.\n In this paper, we present the first symbolic execution technique to support\ngeneral iterated separating conjunctions. We propose a novel representation of\nsymbolic heaps and flexible support for logical specifications that quantify\nover heap locations. Our technique exhibits predictable and fast performance\ndespite employing quantifiers at the SMT level, by carefully controlling\nquantifier instantiations. It is compatible with other features of permission\nlogics such as fractional permissions, recursive predicates, and abstraction\nfunctions. Our technique is implemented as an extension of the Viper\nverification infrastructure.\n