Deduction and Infinite-state Model Checking

Motivation

Q: In `infinite model checking', what is infinite, the model or the checking?

A: Both.

Model checking is an automated method to verify runtime properties of programs. Finite model checking applies to finite abstractions of software systems. Often, the task of constructing appropriate finite abstractions manually is hard, if not impossible. Therefore, a recent and promising research direction aims at infinite model checking. Here, deduction takes the central role in accounting for the infiniteness that arises from the direct modelling of software systems.

So far, the deduction problems arising in this context have been addressed in an adhoc manner by the model checking community. It is interesting to explore where existing techniques can be applied and where new kinds of research questions are raised.

For finite systems, model checking is based on Boolean logic. For many of the classes of systems with specific characteristics for infinite data and infinite control, the question for the right logic is still open (right in terms appropriate expressiveness and computational cost). It will be useful to classify the deduction problems corresponding to the different classes of systems.

Data: What classes of formulas are best used to account for classes of operations over classical domains such as integers? What are the new domains to model pointer structures, lists, queues, abstract data types in general?

Control: Advanced control (recursion, concurrency, threads, dynamic objects with changing communication patterns, mobility of computational agents, ) requires models of process terms with specific algebraic laws (for stack concatenation, parallel composition, ); which ones exactly?

For safety properties, model checking amounts to automatically synthesising inductive invariants, by fixpoint iteration. For infinite model checking, the application of the fixpoint operator, the fixpoint test and the extrapolation of intermediate results each are theorem proving tasks. What are the demands, the functionality, and the evaluation criteria for theorem provers that are called during fixpoint iteration?

For example, the performance of a possibly incomplete decision tool for the validity of implication (used for the fixpoint termination test) determines a tradeoff where the fixpoint iteration terminates after either few but possibly expensive steps or cheap but possibly numerous steps.

Extrapolation of intermediate results during fixpoint iteration is required for accelerating or enforcing termination. The abstract interpretation framework of Cousot and Cousot formulates abstraction techniques at a semantic level. Their instantiation to syntax-based theorem provers is still not obvious.

There are many more possible topics to be discussed at our workshop...