Towards Model-Checking Programs with Lists

8 years 8 months ago
Towards Model-Checking Programs with Lists
Abstract. We aim at checking safety and temporal properties over models representing the behavior of programs manipulating dynamic singly-linked lists. The properties we consider not only allow to perform a classical shape analysis, but we also want to check quantitative aspect on the manipulated memory heap. We first explain how a translation of programs into counter systems can be used to check safety problems and temporal properties. We then study the decidability of these two problems considering some restricted classes of programs, namely flat programs without destructive update. We obtain the following results : (1) the model-checking problem is decidable if the considered program works over acyclic lists (2) the safety problem is decidable for programs without alias test. We finally explain the limit of our decidability results, showing that relaxing one of the hypothesis leads to undecidability results.
Alain Finkel, Étienne Lozes, Arnaud Sangnie
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where ILC
Authors Alain Finkel, Étienne Lozes, Arnaud Sangnier
Comments (0)