Voogd, Erik;
Johnsen, Einar Broch;
Kløvstad, Åsmund Aqissiaq Arild;
Rot, Jurriaan;
Silva, Alexandra;
(2025)
Correct and Complete Symbolic Execution for Free.
In: Kosmatov, Nikolai and Kovács, Laura, (eds.)
Integrated Formal Methods: IFM 2024.
(pp. pp. 237-255).
Springer: Cham, Switzerland.
![[thumbnail of 24-ifm.pdf]](https://discovery.ucl.ac.uk/style/images/fileicons/text.png) |
Text
24-ifm.pdf - Accepted Version Access restricted to UCL open access staff until 14 November 2025. Download (663kB) |
Abstract
Symbolic execution is a powerful technique for program analysis. However, the formal semantics underlying symbolic execution is often developed on an ad-hoc basis and decoupled from the concrete semantics of the programming language. To overcome this issue, we introduce symbolic SOS: a rule format that allows us to simultaneously specify concrete and symbolic operational semantics. We prove that symbolic semantics, when generated from symbolic SOS, is both correct and complete with respect to the corresponding concrete semantics. The approach relies only on an algebraic signature of the source language, and is thus language-independent.
| Type: | Proceedings paper |
|---|---|
| Title: | Correct and Complete Symbolic Execution for Free |
| Event: | 19th International Conference, IFM 2024 |
| ISBN-13: | 978-3-031-76553-7 |
| DOI: | 10.1007/978-3-031-76554-4_13 |
| Publisher version: | https://doi.org/10.1007/978-3-031-76554-4_13 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10203307 |
Archive Staff Only
 |
View Item |
