Reasoning in Combinations of Theories: a Study of Locality

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. The setup considered in this book is that of one base theory which is extended by one or more theories. The question is if and when a given problem in the extended setting can be effectively reduced to an equivalent problem over the base theory. A case where this is always possible is that of so-called local theory extensions. The theory of local extensions is developed and some applications are given. It will be shown that a suitable fragment of both the theory of arrays and the theory of pointers is local as well. Finally, the case of more than one theory extension is discussed. 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.