Supplementary page

Efficient Symbolic Execution using CEGAR over Two Abstract Domains

This is the supplementary web page for the bachelor's thesis on Efficient Symbolic Execution using CEGAR over Two Abstract Domains.

CPAchecker, a framework for configurable software verification used in this work, is available here.

Abstract

Symbolic execution is a powerful approach to automatic software verification we already applied to the domain of configurable software verification in previous work. Unfortunately, it suffers from bad runtime performance, mainly due to path explosion caused by its high precision. To mitigate this problem, we apply counterexample-guided abstraction refinement (CEGAR), an abstraction technique mostly used in model checking, to our configurable program analysis (CPA) for symbolic execution. We design two different refinement procedures for its compositional domain, considering two strongly intertwined domains at the same time. First, applying CEGAR to multiple domains is a novel approach compared to the existing single or combined refinement procedures, which only handle one domain at a time. Second, often seen as two opposites, we are, to our knowledge, the first to apply CEGAR to symbolic execution. Both refinement procedures were implemented in the verification framework CPAchecker and evaluated with different configurations and optimizations to find the one yielding the best results. We are able to show a significant boost in runtime performance compared to symbolic execution without CEGAR for most programs. This concludes CEGAR as a valid mean to improve the runtime performance of symbolic execution and shows a valid way to apply CEGAR to multiple domains.

Results

All executed benchmarks are available as archive including logfiles (79M, prepare for lots of files with long file names) and archive without logfiles (41M). This includes all test results, logfiles and different summaries as html and csv as used in the report. To recreate plots used in the work do not forget to read the README.

The result tables are included in the archive above, but for quick access available are: