Reasoning in combinations of theories

Abstract

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 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 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 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.

Verifikationsaufgaben kombinieren oft verschiedene Theorien. Eine naheliegende Frage ist, ob man Entscheidungsverfahren für die Einzeltheorien auf die gesamte Theorie übertragen kann. In den Fällen, wo das möglich ist, hat man eine mächtige Technik zur Hand, um mit komplexen Theorien effizient umgehen zu können. Der Ansatz, der in dieser Arbeit betrachtet wird, ist stets der einer Hintergrundtheorie, die durch eine oder mehrere Theorien erweitert wird. Die Frage ist dann, ob und wann sich eine gegebene Beweisanfrage bezüglich der Theorieerweiterung effektiv auf eine äquivalente Beweisanfrage bezüglich der Hintergrundtheorie reduzieren lässt. Ein Fall, in dem diese Reduzierung immer möglich ist, ist derjenige der lokalen Theorieerweiterungen. Die Theorie der lokalen Erweiterungen wird entwickelt, und es werden einige Anwendungen für monotone Funktionen gegeben. Danach wird die Theorie der lokalen Erweiterungen verallgemeinert, um mit Datenstrukturen umgehen zu können, die Lokalitätseigenschaften aufweisen. Es wird gezeigt, dass sowohl ein geeignetes Fragment der Theorie der Arrays wie auch der Theorie der Zeiger lokal im erweiterten Sinne sind. Schließlich wird der Fall mehrerer Theorieerweiterungen betrachtet. Insbesondere wird ein Modularitätsresultat gezeigt, das besagt, dass unter gewissen Umständen die Lokalität der einzelnen Erweiterungen hinreichend ist, um die Lokalität der gesamten Erweiterung zu gewährleisten. Die oben erwähnte Reduzierung von Beweisaufgaben ist in jüngster Zeit besonders relevant geworden, weil leistungsfähige Beweiser für gängige Hintergrundtheorien entwickelt worden sind. Diese sogenannten SMT-Beweiser behandeln Theorien wie z.B. lineare Arithmetik der ganzen oder der reellen Zahlen effektiv. Als Teil der vorgelegten Arbeit wurde ein Programm namens H-PILoT entwickelt, welches die Reduzierung von Beweisaufgaben für lokale Theorien durchführt. H-PILoT hat Anwendungen in der Mathematik, bei mehrwertigen Logiken, bei der Verifikation von Datenstrukturen und in der Verifikation komplexer Systeme gefunden.