Correct and Complete Symbolic Execution for Free

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.

Publication
Proc. 19th Intl. Conference on Integrated Formal Methods (IFM 2024). LNCS 15234 © Springer 2024. To appear.
Erik Voogd
Erik Voogd
PhD Student