Software Verification with Program-Graph Interpolation and Abstraction

Abstract

Picture a world where you can ask questions about a piece of code and have tools that automatically and efficiently answer them for you. Can a division by zero ever occur? Are all elements in this list always greater than ten? Does this program always terminate? Are there any race conditions? In such a world, software is considerably more reliable and secure than what we currently have; software has fewer bugs and is easily certifiable like other engineering artifacts; software-induced disasters are effortlessly avoided; and the billions of dollars that are normally spent on testing and maintenance activities are instead poured into more productive endeavours. Alas, such a world is an imaginary utopia, as the majority of these verification questions translate into undecidable problems (due to their relation to the halting problem). Nevertheless, we can still try to design algorithms that answer some questions about programs most of the time, and this is exactly what we do in this dissertation.Specifically, we address the problem of automatically verifying safety properties of programs. Safety properties encompass a wide range of desirable correctness criteria (e.g., no assertions are violated, memory safety, secure information flow, etc.) and form the basis of other verification techniques for liveness properties (like termination). To prove that a program satisfies a safety property, we need to find a safe inductive invariant. A safe inductive invariant characterizes an over-approximation of reachable program states (a valuation of program variables) that does not intersect with unsafe states specified by the property. We advance safety property verification in several directions.First, we target interpolation-based (IB) verification techniques. IB techniques are a new and efficient class of algorithms that avoids traditional abstract fixpoint invariant computation. IB techniques utilize the logical notion of Craig interpolants to hypothesize a safe inductive invariant by examining symbolic executions (finite paths) through the program. We propose DAG interpolants: a novel form of interpolants that facilitates efficient symbolic reasoning about exponentially many program paths represented succinctly as a DAG. In contrast, previous IB techniques explicitly enumerate paths and employ heuristics to avoid path explosion. We show how DAG interpolants can be used to construct efficient safety verification algorithms.Second, we present an extension of McMillan's original IB algorithm [McM06] to the interprocedural iisetting, enabling verification of programs with procedures and recursion. To do so, we introduce the notion of state/transition interpolants, and show how existing interpolant generation techniques can be used for hypothesizing procedure summaries.Third, we propose new verification algorithms that combine abstraction-based (AB) verification techniques, based on abstract domains with fixpoint invariant computation, with IB techniques. Our new algorithms are parameterized by the degree with which AB and IB techniques drive the analysis, providing a spectrum of possible instantiations, and allowing us to harness the advantages of both IB and AB techniques. We experimentally demonstrate the effectiveness of our new hybrid IB/AB techniques and show that our algorithms can outperform state-of-the-art verification techniques from the literature.Finally, we describe the design and implementation of UFOapp, an award-winning tool and framework for C program verification in which we implemented and evaluated our algorithms.