Symbolic verification
of infinite-state systems (past)
Field: symbolic model-checking, infinite state space, acceleration
Applications: embedded systems, protocols, program abstractions
Context
Hardware/software verification is a major challenge for the IT
community. Model-checking is a well-known method, tools exist and
industrial case-studies
have been successfully conducted. However model-checking 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 model-checking 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
case-studies. Another approach is to use semi-algorithms 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
[CAV-03, TACAS-05, CAV-06, STTT-08]
-
Definition of the flat acceleration framework, to unify and clarify the
work done in acceleration [ATVA-05]
- The
composition of symbolic
representations and acceleration to verify heterogeneous systems [ATVA-04]
- First results on the symbolic verification of systems with dynamic memory
allocation [AVIS-04, AVIS-06]
A few slides
Back