Speaker: Tianhai Liu, KIT
Title: A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution,
Abstract:
Constraint solving is a major source of cost in Symbolic Execution (SE).
In this talk, we present a study to assess the importance of some sensible options for solving constraints in SE.
The main observation is that stack-based approaches to incremental solving is often much faster compared to cache-based
approaches, which are more popular. Considering all 96 C programs from the KLEE benchmark that we analyzed, the median
speedup obtained with a (non-optimized) stack-based approach was of 5x.
Results suggest that tools should take advantage of incremental solving support from modern SMT solvers and researchers
should look for ways to combine stack- and cache-based approaches to reduce execution cost even further. Instructions
to reproduce results are available online: http://asa.iti.kit.edu/130_392.php