Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
5-2026
Abstract
The principled combination of symbolic execution and random testing lacks a formal foundation, especially in deciding which inputs to symbolize. We propose selective concolic testing, a cost-aware framework that formulates this choice as an optimized policy problem of a MDP (Markov Decision Process). We model program exploration over a finite control-flow graph, where MDP states represent covered statements, actions partition path constraints into symbolic and random fragments, rewards reflect coverage gain, and costs account for SMT solving effort and sampling inefficiency. Our framework yields the first formal characterization of selective symbolization as policy synthesis in a probabilistic system. We prove that exact policy computation is intractable due to the exponential state space and the hardness of solution-density estimation via model counting. Our formulation enables a practical approximation: we partition constraint dependency graphs and use machine learning to predict solver timeouts, guiding per-constraint symbolization decisions. Built on top of KLEE and JFS, our prototype validates the approach on real-world floating-point benchmarks. Results show that selectively symbolizing inputs, guided by predicted solvability and cost, significantly improves coverage efficiency. Our work thus provides both a rigorous theoretical foundation and a practical instantiation for hybrid program analysis.
Keywords
Concolic Testing, Symbolic Execution, MDP, Constraint Solving
Discipline
Artificial Intelligence and Robotics | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Areas of Excellence
Digital transformation
Publication
Proceedings of the 27th International Symposium, FM 2026, Tokyo, Japan, May 18-22
First Page
275
Last Page
295
ISBN
9783032262196
Identifier
10.1007/978-3-032-26220-2_14
Publisher
Springer
City or Country
Cham
Citation
ZHANG, Guofeng; CHEN, Zhenbang; SHUAI, Ziqi; SUN, Jun; HONG, Weijiang; ZHANG, Yufeng; WANG, Ji; and LIU, Yang.
Selective concolic testing. (2026). Proceedings of the 27th International Symposium, FM 2026, Tokyo, Japan, May 18-22. 275-295.
Available at: https://ink.library.smu.edu.sg/sis_research/11195
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-032-26220-2_14