Publication Type

Journal Article

Version

acceptedVersion

Publication Date

5-2025

Abstract

Symbolic execution is a powerful technique that can accurately synthesize program inputs for program testing through constraint solving. Applying symbolic execution effectively means that we must solve two searching problems efficiently. One is to search through the many program paths and the other is, given a particular path condition, to search through the numerous variable assignments to identify one satisfying solution. With few exceptions, existing symbolic execution engines treat constraint solvers as black boxes. As a result, the two searches are completely separated, which results in much redundancy (i.e., the same variable assignments may be tried for solving many program paths). Existing attempts on addressing this issue include those approaches based on constrained Horn clauses (in which the whole program is encoded as one constraint) and one preliminary attempt on caching and reusing partial solving results from the constraint solver. In this work, we propose SEC, which systematically computes the reward of concretizing a program path (for symbolic execution) and a variable (for constraint solving) and uses the reward as guide for integrating the two searches. We implemented SEC based on KLEE and evaluate it on a diverse set of programs. The results show that SEC is effective, i.e., achieving 15% more code coverage than the state-of-the-art baseline symbolic execution engines. Furthermore, we show that SEC can be readily combined with a state-of-the-art concolic testing engine to improve its performance.

Keywords

Symbolic Execution, SMT Solving, Program Analysis

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Areas of Excellence

Digital transformation

Publication

ACM Transactions on Software Engineering and Methodology

First Page

1

Last Page

28

ISSN

1049-331X

Identifier

10.1145/3735552

Publisher

Association for Computing Machinery (ACM)

Additional URL

https://doi.org/10.1145/3735552

Download

Share

COinS