Event Based Systems in Iași

Symbolic Execution: Revisiting the Solver Chain​
Martin Nowack (TU Dresden)

• Thursday, 22 March 2018, 12:00, C308 (Faculty of Computer Science, C Building, UAIC)

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.

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.

Back to EBSIS Events section.