Hierarchic Decision Procedures for Verification

safety-critical processes, verification of information-processing systems
is becoming increasingly important. Research on automatic or
computer-aided verification is driven by the development of powerful
methods for automated reasoning, in particular decision procedures for
complex combinations of theories that allow us to express the desired
properties in the application domain.

Hierarchic decision procedures decide satisfiability problems in complex
theories by reducing them to equisatisfiable problems in simpler
theories. One approach to do this is reasoning in local theory
extensions, where a given decidable theory is extended with a
universal axiomatization of new function symbols. By finite
instantiation of quantifiers, satisfiability problems in the extended
theory can be reduced to the base theory.

In this talk I will introduce classes of local theory extensions that
allow us to describe interesting systems with a parameterized number
of components, and to decide important verification problems for
these systems. The approach is demonstrated on a sequence of models
taken from a case study of the European Train Control System, with
increasing complexity in the expressivity of the theory extensions, the
control structure of the system, as well as in the underlying track
topology.