Swen Jacobs

"Hierarchic Decision Procedures for Verification"

Zusammenfassung: 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 new function symbols, which are defined by a set of universal axioms. While in general SMT (satisfiability modulo theories) problems containing universally quantified formulas are undecidable, locality of a set of axioms allows us to efficiently reduce satisfiability problems from the extended theory to the base theory by finite instantiation of the axioms.

In this talk I will introduce local theory extensions, give some new extensions that satisfy locality properties, and show how instantiation of axioms can be made more efficient by an incremental, semantically guided procedure. Finally, I will talk about some applications of local reasoning in the verification of parameterized systems.