Paper Info
Title
Compositional invariant checking for overlaid and nested linked lists
Abstract
We introduce a fragment of separation logic, called NOLL, for automated reasoning about programs manipulating overlaid and nested linked lists, where overlaid means that the lists share the same set of objects. The distinguishing features of NOLL are: (1) it is parametrized by a set of user-defined predicates specifying nested linked list segments, (2) a "per-field" version of the separating conjunction allowing to share object locations but not record field locations, and (3) it can express sharing constraints between list segments. We prove that checking the entailment between two NOLL formulas is co-NP complete using a small model property. We also provide an effective procedure for checking entailment in NOLL, which first constructs a Boolean abstraction of the two formulas in order to infer all the implicit constraints, and then, it checks the existence of a homomorphism between the two formulas, viewed as graphs. We have implemented this procedure and applied it on verification conditions generated from several interesting case studies that manipulate overlaid and nested data structures.
Year
DOI
Venue
2013
10.1007/978-3-642-37036-6_9
ESOP
Keywords
Field
DocType
implicit constraint,distinguishing feature,effective procedure,overlaid mean,noll formula,compositional invariant checking,boolean abstraction,automated reasoning,share object location,list segment,nested data structure
Atomic formula,Data structure,Automated reasoning,Separation logic,Logical consequence,Programming language,Linked list,Computer science,Theoretical computer science,Invariant (mathematics),Homomorphism
Conference
Volume
ISSN
Citations 
7792
0302-9743
13
PageRank 
References 
Authors
0.60
18
3
Name
Order
Citations
PageRank
Constantin Enea124926.95
Vlad Saveluc2141.28
Mihaela Sighireanu365837.99