Prof. Dr. Viorica Sofronie-Stokkermans, Universität Koblenz-Landau (slides)

Abstract:

A long term goal of the research in computer science is the analysis and verification of complex systems (these can for instance be programs, reactive or hybrid systems, large databases). ‘In many cases, checking the correctness for such systems can be reduced to reasoning in complex logical theories (for instance, combinations of numerical theories and theories of data types, or certain theories of continuous and/or derivable functions). As the resulting proof tasks are usually large, it is extremely important to have efficient decision procedures for such complex theories.

In this talk we discuss situations in which efficient reasoning in complex theories is possible. We consider a special type of extensions of a base theory, which we call local extensions, where hierarchic reasoning is possible (i.e., we can reduce the task of proving satisfiability of (ground) formulae in the extension to proving satisfiability of formulae in the base theory). We give several examples of theories important for computer science which have this property. We also mention possibilities of symbol elimination in theory extensions and present applications to the verification of parametric systems.