Symbolic verification of infinite-state systems (past)

Field: symbolic model-checking, infinite state space, acceleration
Applications: embedded systems, protocols, program abstractions


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

A few slides