State Merging with Quantifiers in Symbolic Execution

TL;DR

This paper introduces a method to improve symbolic execution by reducing constraint encoding complexity through dynamic state partitioning and quantifier-based encoding, coupled with a specialized solver for efficiency.

Contribution

It presents a novel approach to mitigate constraint explosion in symbolic execution by using quantifiers and a tailored solver, enhancing performance.

Findings

Significant performance improvements demonstrated in evaluations

Effective reduction of disjunctions and if-then-else expressions

Efficient encoding of merged path constraints using quantifiers

Abstract

We address the problem of constraint encoding explosion which hinders the applicability of state merging in symbolic execution. Specifically, our goal is to reduce the number of disjunctions and if-then-else expressions introduced during state merging. The main idea is to dynamically partition the symbolic states into merging groups according to a similar uniform structure detected in their path constraints, which allows to efficiently encode the merged path constraint and memory using quantifiers. To address the added complexity of solving quantified constraints, we propose a specialized solving procedure that reduces the solving time in many cases. Our evaluation shows that our approach can lead to significant performance gains.