“Integrating String Reasoning in Symbolic Execution of C Programs” by Rachel Cleaveland and Clark W. Barrett. In Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II, (Sebastian Junges and Guy Katz, eds.), Apr. 2026, pp. 151-172.
Symbolic execution is a powerful program analysis technique which explores new paths through a program by generating inputs that are guaranteed to exercise those paths. However, there is a lack of modern research on symbolic execution for programs that manipulate strings, especially for C programs. In this work, we develop an approach for symbolically executing string-manipulating C programs and implement it in a proof-of-concept tool called SymCC-str. SymCC-str is built on top of the concolic execution engine SymCC and the smt-switch SMT solving API, enabling it to make use of modern advancements in both symbolic execution and string solving. SymCC-str's novelty lies in its hybrid data representation, expressing symbolic data both as SMT bitvectors and strings in order to balance the performance and expressivity of these respective theories. Through this novel approach, SymCC-str achieves a median 9.9% increase in branch coverage (up to 990% in the best case) compared to SymCC on 6 real-world benchmark programs.
BibTeX entry:
@inproceedings{CB26,
author = {Rachel Cleaveland and Clark W. Barrett},
editor = {Sebastian Junges and Guy Katz},
title = {Integrating String Reasoning in Symbolic Execution of {C}
Programs},
booktitle = {Tools and Algorithms for the Construction and Analysis of
Systems - 32nd International Conference, {TACAS} 2026, Held as
Part of the International Joint Conferences on Theory and Practice
of Software, {ETAPS} 2026, Turin, Italy, April 11-16, 2026,
Proceedings, Part {II}},
series = {Lecture Notes in Computer Science},
pages = {151--172},
publisher = {Springer},
month = apr,
year = {2026},
doi = {10.1007/978-3-032-22749-2_8},
url = {http://theory.stanford.edu/~barrett/pubs/CB26.pdf}
}
(This webpage was created with bibtex2web.)