アイテム詳細

要旨

Verification problems are often expressed in a language which mixes several
theories.
A natural question to ask is whether one can use decision procedures for
individual theories to construct a decision procedure for the union theory.
In the cases where this is possible one has a powerful method at hand to handle
complex theories effectively.

The setup considered in this thesis is that of one base theory which is
extended by one or more theories.
The question is if and when a given ground satisfiability problem in the
extended setting can be
effectively reduced to an equi-satisfiable
problem
over the base theory. A case where this reductive approach is always possible
is that of so-called \emph{local theory extensions.}

The theory of local extensions is developed and some applications concerning
monotone functions are given.
Then the theory of local theory extensions is generalized in order to deal with
data structures that
exhibit local behavior.
It will be shown that a suitable fragment of both the theory of arrays and the
theory of pointers
is local in this broader sense.
%
Finally, the case of more than one theory extension is discussed.
In particular, a \emph{modularity} result is given that under certain
circumstances the locality of each of the extensions
lifts to locality of the entire extension.

The reductive approach outlined above has become particularly relevant
in recent years due to the rise of powerful solvers for background
theories common in verification tasks. These so-called SMT-solvers
effectively handle theories such as real linear or integer arithmetic.
As part of this thesis, a program called \emph{\mbox{H-PILoT}} was
implemented which carries out reductive reasoning for local theory
extensions. H-PILoT found applications in mathematics, multiple-valued
logics, data-structures and reasoning in complex systems.