Name
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-642-03092-5_6 | ILC |
Keywords | Field | DocType |
counter system,alias test,safety problem,considered program work,temporal property,decidability result,model-checking problem,destructive update,classical shape analysis,acyclic list,model checking,shape analysis | Alias,Model checking,Heap (data structure),Theoretical computer science,Decidability,Presburger arithmetic,Memory leak,Mathematics,Shape analysis (digital geometry) | Conference |
Volume | ISSN | Citations |
5489 | 0302-9743 | 3 |
PageRank | References | Authors |
0.38 | 21 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Alain Finkel | 1 | 3 | 0.38 |
| Étienne Lozes | 2 | 121 | 14.32 |
| Arnaud Sangnier | 3 | 236 | 17.99 |