Towards Extending the Applicability of Symbolic Execution

In this talk, we will give an overview of reducing the solving time of symbolic execution by applying incremental solving to it. In the first part of the talk, we show how one can use incremental solving for parallel running solver queries. And in the second part, we will show that combining both, incremental solving and symbolic execution for progressing a single state is not as straight forward as one would expect and can have a negative performance impact. We will present one approach to counteract that behavior and which allows us to combine incremental solving and symbolic execution.

Martin Nowack is a final year Ph.D. student of TU Dresden supervised by Prof. Christof Fetzer in the area of scaling symbolic execution and applying it towards systems research (e.g. in the context of transactional memory). He has been working in the area of optimistic concurrency control using transactional memory in software and hardware in the first place. Later, he changed to symbolic execution. Still, sometimes he tries to combine both worlds.