Symbolic verification
of infinitestate systems (past)
Field: symbolic modelchecking, infinite state space, acceleration
Applications: embedded systems, protocols, program abstractions
Context
Hardware/software verification is a major challenge for the IT
community. Modelchecking is a wellknown method, tools exist and
industrial casestudies
have been successfully conducted. However modelchecking is restricted
to
finite state systems, while in practice sources of infinity are very
common.
For example unbounded counters, channels with parameterized size,
clocks, and
so on.
There are several ways to extend modelchecking to infinite state
systems.
First one can try to isolate decidable subclasses. While it is nice
from a
theoretical point of view, these subclasses are often too restricted
for real
casestudies. Another approach is to use semialgorithms expected to
terminate
in most practical cases. From the past decade, such promising methods
have emerged. They use (1)
symbolic representations to represent in a finite way infinite sets of
concrete values, and (2) widening or acceleration to compute in one
symbolic step an
arbitrary number of steps of the concrete system. The main difference
between
acceleration and widening is that widening aims at termination and
looses
preciseness (with possible spurious warnings) while acceleration
remains exact.
Some results
 Symbolic verification of
systems with unbounded integers through the tool FAST
[CAV03, TACAS05, CAV06, STTT08]

Definition of the flat acceleration framework, to unify and clarify the
work done in acceleration [ATVA05]
 The
composition of symbolic
representations and acceleration to verify heterogeneous systems [ATVA04]
 First results on the symbolic verification of systems with dynamic memory
allocation [AVIS04, AVIS06]
A few slides
Back