Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(5)
Data Structure
Linked Data
Ranking Function
reachability analysis
Safety Properties
Related Publications
(11)
Arithmetic Strengthening for Shape Analysis
Automatic Termination Proofs for Programs with ShapeShifting Heaps
Verifying Programs with Dynamic 1SelectorLinked Structures in Regular Model Checking
Predicate Abstraction and Canonical Abstraction for SinglyLinked Lists
Model Checking Linear Programs with Arrays
Subscribe
Academic
Publications
Programs with Lists Are Counter Automata
Programs with Lists Are Counter Automata,10.1007/11817963_47,Ahmed Bouajjani,Marius Bozga,Peter Habermehl,Radu Iosif,Pierre Moro,Tomás Vojnar
Edit
Programs with Lists Are Counter Automata
(
Citations: 44
)
BibTex

RIS

RefWorks
Download
Ahmed Bouajjani
,
Marius Bozga
,
Peter Habermehl
,
Radu Iosif
,
Pierre Moro
,
Tomás Vojnar
We address the verification problem of programs manipulating one selector
linked data
structures. We propose a new automated approach for check ing safety and termination for these programs. Our approach is based on using counter automata as accurate abstract models: control states correspond to ab stract heap graphs where list segments without sharing are collapsed, and coun ters are used to keep track of the number of elements in these segments. This allows to apply automatic analysis techniques and tools for counter automata in order to verify list programs. We show the effectiveness of our approach, in par ticular by verifying automatically termination of some sorting programs. data structures is a challenging problem. Indeed, the analysis of the behaviour of such programs requires reasoning about complex transformations of data structures involv ing both creation and deletion of objects as well as modifications of the links between them (pointer manipulations). The heap of such programs may have in fact an arbitrary size and shape (a graph structure). There are several approaches for tackling this prob lemaddressingdifferentsubclassesofprogramsandusingdifferentkindsofformalisms for representingand reasoningabout infinite sets of heap structures, e.g., (19,17,21,8). We consider in this paper the class of programs manipulating
linked data
structures with a single datafield selector. It corresponds to programs manipulating linked lists with the possibility of sharing and circularities. We propose a new approach for the au tomatic verification of such programswhich is mainly based on using counter automata as accurate abstract (infinitestate)models. These models can be used for checkingboth
safety properties
and termination of the considered programs using techniques such as (abstract) symbolic
reachability analysis
(for safety and invariance checking) and auto matic generation of decreasing ranking functions (for termination checking). Let us present in more details the proposed approach.We start from the observation that if we do not consider garbage (parts of the heap not reachable from the pointer variables of the program), the heap graph is always a finite collection of graphs of a special form close to a tree: it is either a tree (where edges are directed towards the root) or a set of trees having all their roots connected to a simple cycle. The number of such graphs is infinite, but it can be provedthat for each of them, the numberof vertices where sharing occurs is bounded by the number of pointer variables of the program. ! This work was supported in part by the French Ministry of Research (ACI project Securite Informatique) and the Czech Grant Agency (projects GA CR 102/04/0780 and 102/03/D211).
Conference:
Computer Aided Verification  CAV
, pp. 517531, 2006
DOI:
10.1007/11817963_47
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
www.lsv.enscachan.fr
)
(
www.liafa.jussieu.fr
)
(
www.liafa.jussieu.fr
)
(
dx.doi.org
)
(
www.informatik.unitrier.de
)
More »
Citation Context
(33)
...The literature on regular model checking provides several techniques for overapproximations of the set of reachable heaps to ensure termination, such as widening [20] and specialized abstractions using counters [
6
]...
Rajeev Alur
,
et al.
Streaming transducers for algorithmic verification of singlepass list...
...This work is a full and revised version of the extended abstract [
10
] published in Proceedings of CAV’06...
Ahmed Bouajjani
,
et al.
Programs with lists are counter automata
...Counter machines. Counter machines are ubiquitous computational models that provide a natural class of infinitestate transition systems, suitable for modeling various applications such as broadcast protocols [17], time granularities [10] and programs with pointer variables [
6
], to quote a few examples...
Stéphane Demri
,
et al.
When ModelChecking Freeze LTL over Counter Machines Becomes Decidable
...More recently, driven by complexitytheoretic considerations on the one hand, and potential applications on the other, researchers have investigated additional primitive operations on counters, such as additive updates encoded in binary [
2
,18] or even in parametric form, i.e., whose precise values depend on parameters [3,15]...
...Natural applications of such counter machines include the modelling of resourcebounded processes, programs with lists, recursive or multithreaded programs, and XML query evaluation; see, e.g., [
2
,6,16]...
Stefan Göller
,
et al.
Model Checking Succinct and Parametric OneCounter Automata
...For example, the graph in Figure 4(a) represents a heap containing two lists [4, 0, 5, 2, 3] and [
1
, 4, 3, 6, 2, 3] which share their two last cells...
...Related Work: Invariant synthesis for programs with dynamic data structures has been addressed using different approaches including abstract interpretation [8‐12, 16‐18], Craig interpolants [14], and automatatheoretic techniques [
1
, 3]. The contributions of our paper are (1) a generic framework for combining an abstraction for the heap with various abstraction for data sequences, (2) new abstract domains on data sequences to reason about ...
Ahmed Bouajjani
,
et al.
Invariant Synthesis for Programs Manipulating Lists with Unbounded Dat...
References
(22)
Checking Cleanness in Linked Lists
(
Citations: 49
)
Nurit Dor
,
Michael Rodeh
,
Shmuel Sagiv
Conference:
Static Analysis Symposium/Workshop on Static Analysis  SAS(WSA)
, pp. 115134, 2000
Termination Analysis of Integer Linear Loops
(
Citations: 25
)
Aaron R. Bradley
,
Zohar Manna
,
Henny B. Sipma
Conference:
International Conference on Concurrency Theory  CONCUR
, pp. 488502, 2005
TReX: A Tool for Reachability Analysis of Complex Systems
(
Citations: 65
)
Aurore Annichini
,
Ahmed Bouajjani
,
Mihaela Sighireanu
Conference:
Computer Aided Verification  CAV
, pp. 368372, 2001
Predicate Abstraction and Canonical Abstraction for SinglyLinked Lists
(
Citations: 59
)
Roman Manevich
,
Eran Yahav
,
Ganesan Ramalingam
,
Shmuel Sagiv
Conference:
Verification, Model Checking and Abstract Interpretation  VMCAI
, pp. 181198, 2005
Uber die vollstandigkeit eines gewissen systems der arithmetik ganzer zahlen
(
Citations: 47
)
M. Presburger
Sort by:
Citations
(44)
Streaming transducers for algorithmic verification of singlepass listprocessing programs
(
Citations: 5
)
Rajeev Alur
,
Pavol Černý
Journal:
Sigplan Notices  SIGPLAN
, pp. 599610, 2011
Programs with lists are counter automata
Ahmed Bouajjani
,
Marius Bozga
,
Peter Habermehl
,
Radu Iosif
,
Pierre Moro
,
Tomás Vojnar
Journal:
Formal Methods in System Design  FMSD
, vol. 38, no. 2, pp. 158192, 2011
Proving program termination
Byron Cook
,
Andreas Podelski
,
Andrey Rybalchenko
Journal:
Communications of The ACM  CACM
, vol. 54, no. 5, pp. 8898, 2011
A termination analyzer for Java bytecode based on pathlength
(
Citations: 14
)
Fausto Spoto
,
Fred Mesnard
,
Étienne Payet
Journal:
ACM Transactions on Programming Languages and Systems  TOPLAS
, vol. 32, no. 3, pp. 170, 2010
When ModelChecking Freeze LTL over Counter Machines Becomes Decidable
(
Citations: 4
)
Stéphane Demri
,
Arnaud Sangnier
Conference:
Foundations of Software Science and Computation Structure  FoSSaCS
, pp. 176190, 2010