Combination of Uniform Interpolants for DAPs Verification

In this chapter, we attack the problem of computing covers in theory combinations. Theory combination is an important topic in automated reasoning: it deals with the problem of transferring properties and methods to the union (i.e., the combination) of theories, so as to modularly exploit the properties and the methods of the component theories. The possibility of the transfer to combination is usually one of the desiderata of every automated reasoning methodology, because it avoids developing ad hoc techniques for every theory that can be seen as a combination of theories for which these techniques already exist. Indeed, it allows to operationally exploit the techniques working for the component theories in a modular way (i.e., using these techniques as black boxes) and to lift them to more general machinery that works for the combination. The goal of this chapter is to develop a combined cover algorithm that computes covers for the combination of two theories by employing the cover algorithms of the component theories.