Combining over and under-approximation for program analysis

Static analysis techniques and toolsets have always been mainly designed as over\hyp{}approximation methods to prove program correctness. Recently, the dual approach based on under-approximation has gained attention as a formal basis to prove incorrectness. While these two paradigms can be applied separately, it has been shown that they are also able to cooperate to decide more effectively both correctness and incorrectness properties. In this thesis, we study analogies and differences between over and under-approximation methods to understand what can and cannot be ported from the well studied over-approximation theory to the less studied under-approximation one, and how the two can be combined synergistically. We first focus on abstract interpretation theory, finding limitations in approaches based on under-approximation abstract domains. We then turn our attention to program logics, classifying known results as over or under-approximation and according to the direction of the semantics. In particular, we define a new backward-oriented proof system for under-approximation that exposes sources of errors. Then we present novel extensions that combine over and under-approximations in non-trivial ways, namely Local Completeness Logic and Property Directed Reachability, showing how they improve on the current state of the art for simultaneous correctness and incorrectness analyses.