Bachelor’s Thesis

Hey, good news! After almost a year of other things coming up, my bachelor’s thesis led to my first published research paper! You can find it here:
Dirk Beyer and Thomas Lemberger: Symbolic execution with CEGAR. International Symposium on Leveraging Applications of Formal Methods. Springer, 2016.

My¬†bachelor’s thesis is about¬†Efficient Symbolic Execution using CEGAR over Two Abstract Domains. The implementation is part of CPAchecker, a framework for configurable software verification.

This page is a slightly edited version of the work’s supplementary page.

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 thesis.
To recreate plots do not forget to read the README.

The complete set of result tables is included in the archive above, but some tables are available for quick access, also:

  • Benchmark results for the most important configuration options are available here.
  • Benchmark results for all evaluated sliced path prefix preferences are available here.