Divide, conquer and verify. improving symbolic execution performance
Loading...
Author (Corporation)
Publication date
26.09.2025
Typ of student thesis
Course of study
Collections
Type
05 - Research report or working paper
Editors
Editor (Corporation)
Supervisor
Parent work
Special issue
DOI of the original publication
Link
Series
Series number
Volume
Issue / Number
Pages / Duration
Patent number
Publisher / Publishing institution
arxiv
Place of publication / Event location
Ithaca
Edition
Version
Programming language
Assignee
Practice partner / Client
Abstract
Symbolic Execution is a formal method that can be used to verify the behavior of computer programs and detect software vulnerabilities. Compared to other testing methods such as fuzzing, Symbolic Execution has the advantage of providing formal guarantees about the program. However, despite advances in performance in recent years, Symbolic Execution is too slow to be applied to real-world software. This is primarily caused by the \emph{path explosion problem} as well as by the computational complexity of SMT solving. In this paper, we present a divide-and-conquer approach for symbolic execution by executing individual slices and later combining the side effects. This way, the overall problem size is kept small, reducing the impact of computational complexity on large problems.
Keywords
Event
Exhibition start date
Exhibition end date
Conference start date
Conference end date
Date of the last check
ISBN
ISSN
Language
English
Created during FHNW affiliation
Yes
Strategic action fields FHNW
Publication status
Published
Review
No peer review
Open access category
License
Citation
Scherb, C., Heitz, L., Grieder, H., & Mattmann, O. (2025). Divide, conquer and verify. improving symbolic execution performance. arxiv. https://doi.org/10.48550/arXiv.2310.03598