Contact

Director

Prof. Dr. Ernst-Rüdiger Olderog

Department of Computing Science
FK II
University of Oldenburg
D-26111 Oldenburg, Germany

Coordinator

Ira Wempe

Department of Computing Science
FK II
University of Oldenburg
D-26111 Oldenburg, Germany

[Invited Talk 02.07.2018] Sofronie

Automated Reasoning in Complex Theories and Applications to Verification

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.

(Changed: 20 Jun 2024)  | 
Zum Seitananfang scrollen Scroll to the top of the page