Symbolic execution formally explained

The work

AuthorsFrank S. de Boer; Marcello M. Bonsangue
Editors
Typearticle
Year2021
Citekeyboer2021symbolic

Where it appeared

Published inFormal Aspects of Computing
Volume33
Issue4
Pages617--636

Identifiers

DOI10.1007/s00165-020-00527-y

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 formal model for a basic programming language with 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.

A copy is held

pdf, 298.8 kB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via bibtex
Added2026-08-05 00:00 UTC
Approved bya person 2026-08-16 15:45 UTC

Filed under

deboer fac verifying-real-java

Cite it as

@article{boer2021symbolic,
  title        = {Symbolic execution formally explained},
  author       = {Frank S. de Boer and Marcello M. Bonsangue},
  year         = {2021},
  journal      = {Formal Aspects of Computing},
  volume       = {33},
  number       = {4},
  pages        = {617--636},
  doi          = {10.1007/s00165-020-00527-y},
}

This record lives at https://refs.drheap.org/boer2021symbolic/ and will keep doing so.