eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2007-11-29
1
22
10.4230/DagSemProc.07401.6
article
Local Theory Extensions, Hierarchical Reasoning and Applications to Verification
Sofronie-Stokkermans, Viorica
Ihlemann, Carsten
Jacobs, Swen
Many problems occurring in verification can be reduced to proving
the satisfiability of conjunctions of literals in a background theory.
This can be a concrete theory (e.g. the theory of real or rational numbers),
the extension of a theory with additional functions (free, monotone, or
recursively defined) or a combination of theories. It is therefore very
important to have efficient procedures for checking the satisfiability of
conjunctions of ground literals in such theories.
We present some new results on hierarchical and modular reasoning in
complex theories, as well as several examples of application domains
in which efficient reasoning is possible. We show, in particular,
that various phenomena analyzed in the verification literature can
be explained in a unified way using the notion of local theory extension.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol07401/DagSemProc.07401.6/DagSemProc.07401.6.pdf
Automated reasoning
Combinations of decision procedures
Verification