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

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.

Experiments

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

Install

Installation script: install.sh

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

Run script: run.sh

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.

Results

• rugrat-benchmark-result.csv: It is from testing Rugrat benchmark.
• klee-benchmark-result.csv: It is from testing KLEE benchmark.
• preprocessing-result.csv: It is from evaluating the preprocessing module of the implementation.

BibTex

@InProceedings{Liu-Araujo-dAmorim-Taghdiri-2014,

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}

}