Abstraction is a key technology for proving the correctness of computer programs. There are many approaches available, but unfortunately, the various techniques are difficult to combine and the successful techniques have to be re-implemented again and again.

We address this problem by using the tool CEGAR-PT, which views abstraction as program transformation and integrates different verification components off-the-shelf. The idea is to use existing components without having to change their implementation, while still adjusting the precision of the abstraction using the successful CEGAR approach. The approach is largely general: it only restricts the abstraction to transform, given a precision that defines the level of abstraction, one program into another program. The abstraction by program transformation can over-approximate the data flow (e.g., havoc some variables, use more abstract types) or the control flow (e.g., loop abstraction, slicing). Demonstration video: https://youtu.be/ASZ6hoq8asE

Dirk Beyer

LMU Munich

Germany

Marian Lingsch-Rosenfeld

LMU Munich

Martin Spiessl

LMU Munich

Germany

Loop abstraction is a central technique for program analysis, because loops can cause large state spaces if they are unfolded. In many cases, simple tricks can accelerate the program analysis significantly. There are several successful techniques for loop abstraction, but they are hard-wired into different tools and therefore difficult to compare and experiment with. We present a framework that allows us to implement loop abstractions in one common environment, where each technique can be freely switched on and off on-the-fly during the analysis. We treat loops as part of the abstract model of the program, and use counterexample-guided abstraction refinement to increase the precision of the analysis by dynamically selecting particular techniques for loop abstraction. The framework is independent from the underlying abstract domain of the program analysis, and can therefore be used for several different program analyses. Furthermore, our framework can transform the input program to a modified C program that is unsafe if the input program is unsafe. This allows loop abstraction to be used by other verifiers and our improvements are not `locked in’ to our verifier. We implemented several existing approaches and evaluate their effects on the program analysis.

Marian Lingsch-Rosenfeld

LMU Munich