Paper Info
Title
Verification of Dynamic Data Tree with mu-calculus Extended with Separation
Abstract
The problem of verifying software systems that use dynamic data structures (such as linked lists, queues, or binary trees) has attracted increasing interest over the last decade. Dynamic structures are barely supported by verification techniques because among other reasons, it is difficult to efficiently manage the pointer-based internal representation. This is a key aspect when the goal is to construct a verification tool based on model checking techniques, for instance. In addition, since new nodes may be dynamically inserted or extracted from the structure, the shape of the dynamic data (and other more specific properties) may vary at runtime, it being difficult to detect errors such as, for instance, the non desirable sharing between two nodes. In this paper, we propose to use mu-calculus to describe and analyze, using model checking techniques, dynamic data such as lists, and non-linear data structures like trees. The expressiveness of mu-calculus makes it possible to naturally describe these structures. In addition, following the ideas of separation logic, the logic has been extended with a new operator able to describe the non-sharing property which is essential when analyzing data structures of this type.
Year
DOI
Venue
2010
10.1109/SEFM.2010.34
SEFM
Keywords
Field
DocType
data structure,formal logic,software systems,tree data structures,data models,computer languages,lambda calculus,shape,dynamic data,data structures,separation logic,binary tree,model checking
Data structure,Pointer (computer programming),Separation logic,Programming language,Linked list,Model checking,Computer science,Tree (data structure),Theoretical computer science,Runtime verification,Dynamic data
Conference
Citations 
PageRank 
References 
2
0.36
16
Authors
2
Name
Order
Citations
PageRank
María del Mar Gallardo114113.16
David Sanán27216.51