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 firstorder logic. © 2006 IEEE.

A theory of singly-linked lists and its extensible decision procedure / Ranise, S.; Zarba, C.. - (2006), pp. 206-215. (Intervento presentato al convegno 4th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2006 tenutosi a Pune, ind nel 2006) [10.1109/SEFM.2006.7].

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

Ranise S.;
2006-01-01

Abstract

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 firstorder logic. © 2006 IEEE.
2006
Proceedings - 4th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2006
United States
IEEE
0-7695-2678-0
Ranise, S.; Zarba, C.
A theory of singly-linked lists and its extensible decision procedure / Ranise, S.; Zarba, C.. - (2006), pp. 206-215. (Intervento presentato al convegno 4th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2006 tenutosi a Pune, ind nel 2006) [10.1109/SEFM.2006.7].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333130
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 25
  • ???jsp.display-item.citation.isi??? ND
social impact