Symbolic execution formally explained
Formal Aspects of Computing, vol. 33, pp. 617–636
Abstract
Abstract In this paper, we provide a formal explanation of symbolic execution in terms of a symbolic transition system and prove its correctness and completeness with respect to an operational semantics which models the execution on concrete values.We first introduce a formalmodel for a basic programming languagewith a statically fixed number of programming variables. This model is extended to a programming language with recursive procedures which are called by a call-by-value parameter mechanism. Finally, we present a more general formal framework for proving the soundness and completeness of the symbolic execution of a basic object-oriented language which features dynamically allocated variables.
Authors 2
-
Leiden University · Centrum Wiskunde & Informatica
Affiliation as printed
Centrum Wiskunde and Informatica (CWI), Leiden, The Netherlands
Leiden Institute Of Advanced Computer Science (LIACS), Leiden University, Leiden, The Netherlands
-
Affiliation as printed
Leiden Institute Of Advanced Computer Science (LIACS), Leiden University, Leiden, The Netherlands
Cited by 13 stored of 13
13 results
No patents citing this paper on Lens.org (checked 2026-10-11).