A theory of singly-linked lists and its extensible decision procedure

The key to many approaches to reason about pointer-based data structures is the availability of a decision proce-dure to automatically discharge proof obligations in a the-ory encompassing data, pointers, and the reachability re-lation induced by pointers. So far, only approximate so-lutions have been proposed which abstract either the data or the reachability component. Indeed, such approxima-tions cause a lack of precision in the verication techniques where the decision procedures are exploited. In this paper, we consider the pointer-based data struc-ture of singly-linked lists and dene a Theory of Linked Lists (TLL). The theory is expressive since it is capable of precisely expressing both data and reachability constraints, while ensuring decidability. Furthermore, its decidability problem is NP-complete. We also design a practical deci-sion procedure for TLL which can be combined with a wide range of available decision procedures for theories in rst-order logic. 1