|
Published Articles >> Table of Contents >> Abstract
Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06)
pp. 206-215
A Theory of Singly-Linked Lists and its Extensible Decision Procedure
Silvio Ranise, LORIA-INRIA - Lorraine
Calogero Zarba, Universitat der Saarlandes
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2006.7
Send link to a friend
| Abstract |
|
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 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 firstorder
logic.
|
 Additional Information
|
Citation:
Silvio Ranise, Calogero Zarba,
"A Theory of Singly-Linked Lists and its Extensible Decision Procedure,"
sefm,
pp. 206-215,
Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM'06),
2006
|
|
