Divide, conquer and verify. improving symbolic execution performance
Lade...
Autor:in (Körperschaft)
Publikationsdatum
26.09.2025
Typ der Arbeit
Studiengang
Typ
05 - Forschungs- oder Arbeitsbericht
Herausgeber:innen
Herausgeber:in (Körperschaft)
Betreuer:in
Übergeordnetes Werk
Themenheft
DOI der Originalpublikation
Link
Reihe / Serie
Reihennummer
Jahrgang / Band
Ausgabe / Nummer
Seiten / Dauer
Patentnummer
Verlag / Herausgebende Institution
arxiv
Verlagsort / Veranstaltungsort
Ithaca
Auflage
Version
Programmiersprache
Abtretungsempfänger:in
Praxispartner:in/Auftraggeber:in
Zusammenfassung
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.
Schlagwörter
Veranstaltung
Startdatum der Ausstellung
Enddatum der Ausstellung
Startdatum der Konferenz
Enddatum der Konferenz
Datum der letzten Prüfung
ISBN
ISSN
Sprache
Englisch
Während FHNW Zugehörigkeit erstellt
Ja
Zukunftsfelder FHNW
Publikationsstatus
Veröffentlicht
Begutachtung
Keine Begutachtung
Open Access-Status
Lizenz
Zitation
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