Software Verification by Combining Program Analyses of Adjustable Precision

In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers, on one hand, are still mostly concerned with precision, e.g., the removal of spurious counterexamples. Lattice-based program analyzers, on the other hand, are primarily concerned with efficiency. To achieve their respective goal, the former builds and refine reachability tress while the latter annotates location with abstract states and rely on overapproximation to accelerate convergence. In this thesis we focus on capturing within a framework existing approaches as well as new solutions with the objective of enabling a better understanding of the fundamental similarities and differences between approaches and with a strong accent on implementability. In a first step, we designed and implemented a framework and a corresponding algorithm for software verification called configurable program analysis. The algorithm can be configured to perform not only a purely tree-based or a purely lattice-based analysis, but offers many intermediate settings that have not been evaluated before. An instance of an analysis in the framework consists of one or more program analyses, such as a predicate abstraction or a shape analysis, and their execution and interaction is controlled using several parameters of our generic verification algorithm. Our experiments consider different configurations of combinations of symbolic analyses. By varying the value of parameters we were able to explore a continuous precision-efficiency spectrum and we showed that it can lead to dramatic improvements in efficiency. In a second step, we improved our framework and algorithm to enable the program analysis to dynamically (on-line) adjust its precision depending on the accumulated results. The framework of configurable program analysis offers flexible, but static, composition of program analyses. Our extension enables composite analyses to adjust the precision of each of their component analyses independently and dynamically. To illustrate, we can allow the explicit tracking of the values of a variable to be switched off in favor of a predicate abstraction when and where the number of different variable values that have been encountered has exceeded a specified threshold. We evaluated the dynamic precision adjustment mechanism by considering combinations of symbolic and explicit analyses. We analyzed code taken from an SSH client/server software as well as hand-crafted examples. We showed that the new approach offers significant gains compared with a purely symbolic, predicate-abstraction-based approach. In a third step, we consider the problem of refinement in addition to the dynamic adjustment of the precision. In contrast to precision adjustment, refinement only increases the precision of the analysis. Moreover, when a refinement occurs, states with a lower precision are discarded and replaced by states with a higher precision. Based on our framework, we present a novel refinement approach for shape analysis, a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structure implementations. The approach uses two techniques to guide the refinement of shape abstractions. First, during program exploration, an explicit heap analysis collects sample instances of the heap structures. The samples are used to identify the data structures that are manipulated by the program. Second, during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We were able to successfully verify example programs from a data-structure library that manipulate doubly-linked lists and trees. The techniques presented in this thesis have been implemented as an extension to the BLAST model checker.