Campus Event Calendar

Event Entry

New for: D3

What and Who

Hierarchic Decision Procedures for Verification

Swen Jacobs
AG 1, AG 3, AG 5, SWS, AG 4, RG1, MMCI  
Expert Audience

Date, Time and Location

Thursday, 7 April 2011
90 Minutes
E1 3


With the advent of ubiquitous computing and the increased automation of

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


Prof. Sebastian Hack
--email hidden
passcode not visible
logged in users only

gk-sek, 04/01/2011 08:51 -- Created document.