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

Programs with Lists Are Counter Automata   (Citations: 44)
BibTex | RIS | RefWorks Download
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 data-field 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 (infinite-state)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. 517-531, 2006
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.
    • ...The literature on regular model checking provides several techniques for over-approximations of the set of reachable heaps to ensure termination, such as widening [20] and specialized abstractions using counters [6]...

    Rajeev Aluret al. Streaming transducers for algorithmic verification of single-pass list...

    • ...This work is a full and revised version of the extended abstract [10] published in Proceedings of CAV’06...

    Ahmed Bouajjaniet al. Programs with lists are counter automata

    • ...Counter machines. Counter machines are ubiquitous computational models that provide a natural class of infinite-state 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 Demriet al. When Model-Checking Freeze LTL over Counter Machines Becomes Decidable

    • ...More recently, driven by complexity-theoretic 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 resource-bounded processes, programs with lists, recursive or multi-threaded programs, and XML query evaluation; see, e.g., [2,6,16]...

    Stefan Gölleret al. Model Checking Succinct and Parametric One-Counter 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 automata-theoretic 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 Bouajjaniet al. Invariant Synthesis for Programs Manipulating Lists with Unbounded Dat...

Sort by: