Symbolic Execution with CEGAR in CPAchecker

Thomas Lemberger (University of Passau)

When: Monday June 12, 2pm

Where: room C417 (at the very end of the corridor)

Abstract

In the field of software analysis, there are a few techniques that are reused frequently by different approaches, e.g., building a control flow graph, computing a dependency graph or integrating different SMT solvers. Often, these techniques are reimplemented or third-party tools providing these techniques have to be integrated, which increases development time and makes implementations of approaches less comparable. CPAchecker is a framework for configurable program analysis of C programs that provides many prominent concepts of the field of software verification for easy use. If approaches are implemented in the existing infrastructure of CPAchecker, their differences are better comparable and implementation time is decreased. Multiple successful approaches to software verification and other fields of software engineering were implemented this way, already. In the context of CPAchecker, a symbolic execution analysis is implemented which successfully uses counterexample-guided abstraction refinement to mitigate the path explosion problem. This talk will give an introduction to the general concepts of CPAchecker and its modular architecture, present the symbolic execution analysis implemented in CPAchecker and how CEGAR influences its behavior.