Verification of complex dynamic data tree with mu-calculus

摘要

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 not easily 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, for instance, the goal is to construct a verification tool based on model checking techniques. In addition, since new nodes can be dynamically inserted or extracted from the structure, the shape of the dynamic data (and other more specific properties) may vary at runtime, with errors such as the non desirable sharing between two nodes being difficult to detect. In this paper, we propose to use mu-calculus to describe and analyze with model checking techniques dynamic data structures such as lists and 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 capable of describing the non-sharing property, which is essential when analyzing dynamic data structures.