Official LSV Web Site
Research
Field: symbolic model-checking, infinite state space, accelerations.
Applications: embedded systems, protocols, program abstractions.
A short
introduction (in French).
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.
Projects
- Workgroup Persée (collaboration between LABRI, LIAFA and LSV). Verification of heterogeneous systems, especially integration of
existing tools via a generic model-checker architecture. Funded by French government. 2003-2006.
- Contract with ÉDF. Verification of programs manipulating dynamic memory. 2002-2003.
Some results
-
Definition of the flat acceleration framework, to unify and clarify the work done in acceleration (slides).
- Symbolic verification of
systems with unbounded integers through the tool FAST (slides). FAST is a tool for computing the
reachability set of automata extended with unbounded integers. The tool was
presented at [CAV'03], with lots of encouraging case studies. A better
acceleration algorithm and a complex case-study were presented at [TACAS'04].
- The
composition of symbolic
representations and acceleration to verify heterogeneous systems.
This is part of a contract with the French
research department ( ACI
Persée). See this paper (ATVA'04) for a
first work, and the corresponding slides.
- The
verification of systems with dynamic memory allocation. [AVIS'04]
introduces pointer automata and a promising symbolic representation for it.
This work was a preliminary study, under contract with EDF (French
electricity supplier).
Current interests
- Scale up accelerations to wider systems (abstraction)
- Develop accelerations for heterogeneous hybrid systems
- Software verification
Talks