Automated Software Analysis Group

A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution

  • Author:

    Tianhai Liu, Mateus Araujo, Marcelo d‘Amorim, Mana Taghdiri

  • Place:

    10th Haifa Verification Conference (HVC), 2014

  • 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.


    This section shows the instructions to run the experiments. We are pleased to provide help if you have problems. 


    Installation script:

    This script will help you to automatically setup the experiments. It will download and decompress the implementation and benchmarks used in the experiments of this paper.


    Run script:

    This script will run all experiments of this paper. It will generated time breakdown files (as below) and JUnit test cases for the analyzed methods.

    System requirements to run all benchmarks:
    1. A 64-bit Linux machine with at least 8 GB RAM.
    2. JDK 1.7 runtime.
    3. Disk size at least 100 GB to store all generated test cases.


    The results of our experiments in this paper are:




    author = {Tianhai Liu and Mateus Araujo and Marcelo d'Amorim and Mana Taghdiri},

    title = {A Comparative Study of Incremental Constraint Solving Approaches in Symbolic Execution},

    booktitle = {10th Haifa Verification Conference (HVC), 2014},

    year = {2014},

    month = {November}