Abstraction refinement techniques for software model checking

Software model checking is a promising approach for the automatic verification of software systems. Many tools based on this approach have been implemented and successfully applied to real world programs. Program abstraction is the key to the effectiveness of software model checking. Most of the existing software model checkers are based on the counterexample guided abstraction refinement paradigm, commonly known as CEGAR, to efficiently abstract programs. Starting with a coarse abstraction, the CEGAR paradigm permits to iteratively refine this abstraction until reaching an abstraction which is sufficiently precise to prove the property of interest. A problem common to most of the existing tools is the divergence of CEGAR in the presence of loops. In particular, infinitely many (spurious) counterexamples may arise from unfolding the same loop in a given program again and again. This problem is due to the inefficiency of the abstraction refinement mechanisms used by these tools. The aim of this dissertation is the enhancement of the CEGAR process by tackling the divergence problem from different sides. First, we introduce loop summaries, an approach that goes beyond the abstraction of program states by abstracting transition relations induced by program loops over program states. Such an abstraction permits to shortcut an infinite sequence of refinement steps. We provide experimental evidence showing how loop summaries boost the CEGAR process. Next, we treat quantified assertions over arrays. Quantified assertions are used to express properties over a (infinite) collection of array elements. We claim that careful adaptation of existing software model checking techniques is sufficient to verify many interesting properties over arrays. We support our claim by presenting a method for reasoning about (unbounded) array segments. The underlying ingredients of our technique are standard to most software model checkers. This makes our technique easily integrable to other tools. Despite its simplicity our approach is surprisingly effective, it allowed us to successfully verify quantified array assertions for both text book examples (selection sort) and real-life examples taken from system code (e.g., device driver and kernel code). Finally, we treat the modularity aspect regarding the verification of quantified array assertions. We present a method based on assume guarantee reasoning to reduce the complexity of the verification task. The reduction affects the code as well as the assertion to be verified. The implementation of this method consists of a source-to-source transformation. The application of this technique did not only improve performance of our tool but also enabled us to verify examples that are challenging for automatic verification tools, such as insertion sort and bubble sort, in addition to selection sort. To the best of our knowledge, there is only one work in the literature proposing a method to handle these three sorting algorithms automatically. We implemented ACSAR a software model checker for C programs. All techniques presented in this thesis have been integrated into ACSAR. We provide an experimental study for each technique.