Sciweavers

Share
SEFM
2006
IEEE

A Theory of Singly-Linked Lists and its Extensible Decision Procedure

10 years 5 months ago
A Theory of Singly-Linked Lists and its Extensible Decision Procedure
The key to many approaches to reason about pointerbased 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 sohave 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 firstorder logic.
Silvio Ranise, Calogero G. Zarba
Added 12 Jun 2010
Updated 12 Jun 2010
Type Conference
Year 2006
Where SEFM
Authors Silvio Ranise, Calogero G. Zarba
Comments (0)
books