Towards Model-Checking Programs with Lists

摘要

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.