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 procedure to automatically discharge proof obligations in a theory encompassing data, pointers, and the reachability relation induced by pointers. So far, only approximate solutions have been proposed which abstract either the data or the reachability component. Indeed, such approximations cause a lack of precision in the verification techniques where the decision procedures are exploited. In this paper, we consider the pointer-based data structure of singly-linked lists and define 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 decision procedure for TLL which can be combined with a wide range of available decision procedures for theories in first order logic