My master’s thesis is titled Abstraction Refinement for Model Checking: Program Slicing + CEGAR. The implementation is part of CPAchecker, a framework for configurable software verification.
You can find more information on this work on its supplementary web page!
Program slicing and counterexample-guided abstraction (CEGAR) are two established approaches to program abstraction in software verification. Both are similar in their concept, with one main difference: Program slicing works on the syntactic level, while CEGAR works on the semantic level. Because of the complexity of software and the complex behavior of the two algorithms, the difference in the capabilities of the two is not clear. To contribute towards understanding this technique, we design a program slicing technique that is based on CEGAR and that performs program slicing on dynamically computed slicing criteria. We implement this technique in the widely used software verification framework CPAchecker, and extend it to be combine-able with any other, existing abstraction refinement based on CEGAR. As a proof of concept, we combine it with the CEGAR-based symbolic execution engine in CPAchecker. In a next step, we extend the existing state-of-the-art, LLVM-based program slicer Symbiotic to use CPAchecker as a verification back-end. To combine theses two tools, we also implement a new LLVM front-end in CPAchecker that enables CPAchecker to analyze LLVM programs. As a last step, to get a better understanding of the behavior of our analyses, we implement an abstract graph visualization technique, called pixel trees. Pixel trees allow users to grasp the structure of the programstate space that got explored by an analysis run, even for graphs that are too large to comprehend in a detail view. We perform a thorough evaluation of all presented techniques. Through this, we are able to show that program slicing and CEGAR are two complementing technologies, and that their combination can have a significant impact on verification performance.