Symbolic Execution: Revisiting the Solver Chain
-----------------------------------
          
This seminar is part of the "EBSIS - Event Based Systems in Iasi"
Twinning project.
This project has received funding from the European Union's Horizon 2020
research and innovation programme under grant agreement No 692178.
-----------------------------------
          
ABSTRACT
-----------------------------------
KLEE is a state-of-the-art symbolic execution engine 
that applies a set of optimizations including different 
simplification steps (expression simplification, 
independence calculation) and caching (simple validity 
caching, counterexample caching) before it calls the solver. 
In the original paper, this had a tremendous impact on 
the solving process. We want to present a closer look 
into the solver chain analyzing the impact of the chain 
in different scenarios. We will present a detailed 
performance analysis of the core utils benchmark. 
Starting from there, we propose different optimizations 
and additional caching strategies and show how they can 
lead to potential performance improvements.
          
SPEAKER(S)
-----------------------------------
NOWACK Martin
TU Dresden
Germania
-----------------------------------
Martin Nowack received his Diploma in Computer Science 
from TU Dresden in 2009 and is a research assistant 
since then at the systems engineering chair at TU Dresden. 
He is a final year Ph.D. student. 
His research interests are software validation and testing 
using symbolic execution; and multi-core programming with a 
focus on transactional memory.
He is a maintainer and active contributor of the open 
source symbolic execution engine KLEE.
-----------------------------------