Abstraction for Shape Analysis with Fast and Precise Transformers

摘要: This paper addresses the problem of proving safety properties imperative programs manipulating dynamically allocated data structures using destructive pointer updates. We present a new abstraction for linked whose underlying graphs do not contain cycles. The is simple and allows us to decide reachability between heap cells. We an efficient algorithm that computes effect low level mutations in most precise way. does rely on usage theorem prover. In particular, worst case complexity computing single successor abstract state O(V logV) where V number program variables. overall states can be exponential V. A prototype was implemented shown fast. Our method also handles with “simple cycles” such as cyclic singly-linked lists, (cyclic) doubly-linked trees parent pointers. Moreover, we allow which temporarily violate these restrictions long they are restored loop boundaries.