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.

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

Ranise, Silvio;
2006

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.
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: http://hdl.handle.net/11582/22089
 Attenzione

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

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