eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-11-09
6081
1
18
10.4230/DagSemProc.06081.1
article
06081 Abstracts Collection – Software Verification: Infinite-State Model Checking and Static Program Analysis
Abdulla, Parosh Aziz
Bouajjani, Ahmed
Müller-Olm, Markus
From 19.02.06 to 24.02.06, the Dagstuhl Seminar 06081 ``Software Verification: Infinite-State Model Checking and Static Program Analysis'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl.
During the seminar, several participants presented their current
research, and ongoing work and open problems were discussed. Abstracts of
the presentations given during the seminar
are put together in this paper. The first section
describes the seminar topics and goals in general.
Links to extended abstracts or full papers are provided, if available.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol06081/DagSemProc.06081.1/DagSemProc.06081.1.pdf
Software verification
infinite-state systems
static program analysis
automatic analysis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-11-09
6081
1
5
10.4230/DagSemProc.06081.2
article
06081 Executive Summary – Software Verification: Infinite-State Model Checking and Static Program Analysis
Abdulla, Parosh Aziz
Bouajjani, Ahmed
Müller-Olm, Markus
{\em Software systems} are present at the very heart of many daily-life
applications,
such as in communication (telephony and mobile Internet),
transportation, energy, health, etc.
Such systems are very often {\em critical}\/ in the sense that their failure
can have considerable human/economical consequences.
In order to ensure reliability,
development methods must include {\em algorithmic analysis and verification
techniques}
which allow (1) to detect automatically defective behaviors of the system
and to analyze their source, and (2) to check that every component of a
system
conforms to its specification.
Two important and quite active research communities are particularly
concerned with this challenge:
the community of computer-aided verification, especially the community of
(infinite-state) model checking, and the community of static program
analysis.
From 19.02.06 to 24.02.06,
51 researchers from these two communities
met at the
Dagstuhl Seminar 06081 ``Software Verification: Infinite-State Model Checking and Static Program Analysis''
in order to improve and deepen the mutual
understanding of the developed technologies and to trigger
collaborations.
During the seminar which was held at the
International Conference and Research Center (IBFI),
Schloss Dagstuhl,
several participants presented their current research, and ongoing
work and open problems were discussed. Abstracts of the presentations
given during the seminar are put together in this paper.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol06081/DagSemProc.06081.2/DagSemProc.06081.2.pdf
Infinite-state systems
model checking
program analysis
software verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-11-09
6081
1
25
10.4230/DagSemProc.06081.3
article
Analysis of Dynamic Communicating Systems by Hierarchical Abstraction
Bauer, Jörg
Wilhelm, Reinhard
We propose a new abstraction technique for verifying topology properties
of dynamic communicating systems (DCS), a special class of infinite-state
systems. DCS are characterized by unbounded creation and destruction of
objects along with an evolving communication connectivity or topology.
We employ a lightweight graph transformation system to specify DCS.
Hierarchical Abstraction (HA) computes a bounded over-approximation of
all topologies that can occur in a DCS directly
from its transformation rules. HA works in two steps.
First, for each connected component, called cluster, of a topology,
objects sharing a common property are summarized to one abstract object.
Then isomorphic abstract connected components are summarized to
one abstract component, called abstract cluster.
This yields a conservative approximation of all graphs that may occur
during any DCS run.
The technique is implemented.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol06081/DagSemProc.06081.3/DagSemProc.06081.3.pdf
Graph transformation
Abstract Interpretation
Shape Analysis
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-11-09
6081
1
19
10.4230/DagSemProc.06081.4
article
Flat counter automata almost everywhere!
Leroux, Jérôme
Sutre, Grégoire
This paper argues that flatness appears as a central notion in the
verification of counter automata. A counter automaton is called flat
when its control graph can be ``replaced'', equivalently w.r.t.
reachability, by another one with no nested loops.
From a practical view point, we show that flatness is a necessary and
sufficient condition for termination of accelerated symbolic model
checking, a generic semi-algorithmic technique implemented in
successful tools like FAST, LASH or TReX.
From a theoretical view point, we prove that many known semilinear
subclasses of counter automata are flat: reversal bounded counter
machines, lossy vector addition systems with states, reversible Petri nets,
persistent and conflict-free Petri nets, etc. Hence, for these subclasses,
the semilinear reachability set can be computed using a emph{uniform}
accelerated symbolic procedure (whereas previous algorithms were
specifically designed for each subclass).
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol06081/DagSemProc.06081.4/DagSemProc.06081.4.pdf
Symbolic representation
Infinite state system
Acceleration
Meta-transition
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-11-09
6081
1
16
10.4230/DagSemProc.06081.5
article
Lazy Shape Analysis
Beyer, Dirk
Henzinger, Thomas A.
Théoduloz, Grégory
Many software model checkers are based on predicate abstraction. If
the verification goal depends on pointer structures, the approach does
not work well, because it is difficult to find adequate predicate
abstractions for the heap. In contrast, shape analysis, which uses
graph-based heap abstractions, can provide a compact representation of
recursive data structures. We integrate shape analysis into the
software model checker BLAST. Because shape analysis is expensive, we
do not apply it globally. Instead, we ensure that, like predicates,
shape graphs are computed and stored locally, only where necessary for
proving the verification goal. To achieve this, we extend lazy
abstraction refinement, which so far has been used only for predicate
abstractions, to three-valued logical structures. This approach does
not only increase the precision of model checking, but it also
increases the efficiency of shape analysis. We implemented the
technique by extending BLAST with calls to TVLA.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol06081/DagSemProc.06081.5/DagSemProc.06081.5.pdf
Software model checking
Shape analysis
Counterexample-guided abstraction refinement
Interpolation
Predicate abstraction
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2006-11-09
6081
1
18
10.4230/DagSemProc.06081.6
article
Reachability analysis of multithreaded software with asynchronous communication
Bouajjani, Ahmed
Esparza, Javier
Schwoon, Stefan
Strejcek, Jan
We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent pushdown systems) and DPN (dynamic pushdown networks). We show that ADPN exhibit several advantages as a program model. Since the reachability problem for ADPN is undecidable even in the case without dynamic creation of processes, we address the bounded reachability problem, which considers only those computation sequences where the (index of the)
thread accessing the shared memory is changed at most a fixed given
number of times. We provide efficient algorithms for both forward and
backward reachability analysis. The algorithms are based on automata techniques for symbolic representation of sets of configurations.
This talk is based on joint work with Ahmed Bouajjani, Javier Esparza, and Jan Strejcek that appeared in FSTTCS 2005.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol06081/DagSemProc.06081.6/DagSemProc.06081.6.pdf
Model checking
pushdown systems
concurrency