A comparative study of incremental constraint solving approaches in symbolic execution

T Liu, M Araújo, M d'Amorim, M Taghdiri - Hardware and Software …, 2014 - Springer
T Liu, M Araújo, M d'Amorim, M Taghdiri
Hardware and Software: Verification and Testing: 10th International Haifa …, 2014Springer
Constraint solving is a major source of cost in Symbolic Execution (SE). This paper presents
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 …
Abstract
Constraint solving is a major source of cost in Symbolic Execution (SE). This paper presents 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
Springer