Symbolic Execution, Path Conditions, and Concolic Testing

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

Run the following program at input $-2$. It takes the left branch and the assertion succeeds. That run says nothing about the right branch. Run it at input $4$, and the right branch reaches a failed assertion. $$\begin{array}{}\text{(}\mathsf{Fork}\text{)}& \begin{array}{l}\mathbf{input}x;\\ \mathbf{if}x\le 0\mathbf{then}y:=x+1\mathbf{else}y:=x-1;\\ \mathbf{assert}y\le 2.\end{array}\end{array}$$ An interval execution beginning with $x\in [-\mathrm{\infty },+\mathrm{\infty }]$ joins the two stores at the end of the conditional. It may retain a safe over-approximation of $y$, but it no longer carries the concrete equation relating $x$ to the selected branch. To generate the failing test, we instead keep one store per path and a formula describing the inputs on that path.

This chapter fixes a deliberately small calculus, SymImp-DL. Its constraints are decidable by checkable difference-logic certificates. That choice puts the proof boundary in the open: an untrusted solver may propose a model, a negative cycle, or unknown; only the first two are accepted after local checking.

Concrete commands and symbolic integers

Let $x,y,z$ range over a finite set $\mathsf{Var}$, $k$ over integers, and ${\alpha }_i$ over input symbols. Concrete right-hand sides and guards are $$a::=k\mid x+k,g::=a_1-a_2\le k.$$ The notation includes $x\le k$ by taking $a_2=0$, and $x=y+k$ as two inequalities. Commands are Assignments are intentionally only copy-plus-constant. This closure property ensures that substituting a symbolic store into a guard again yields difference logic.

A concrete store is a total map $s:\mathsf{Var}\to \mathbb{Z}$. An input oracle $I:\mathbb{N}\to \mathbb{Z}$ fixes a run, and a cursor $n$ records the next unread input. We write $⟨c,s,I,n⟩{⟶}_{\mathsf{c}}⟨c^{\prime },s^{\prime },I,n^{\prime }⟩$; failed assertions step to $\mathsf{fail}(s,I,n)$. Assignment, input, conditionals, assertions, and while-unfolding have the expected rules; sequencing propagates a step and erases a leading $\mathbf{skip}$. Appendix A displays the complete rules.

A symbolic integer is $$t::=k\mid {\alpha }_i+k.$$ A symbolic store $\sigma :\mathsf{Var}\to \mathsf{STerm}$ maps variables to such terms. A valuation $\rho :\mathbb{N}\to \mathbb{Z}$ evaluates terms by $[[k{]]}_{\rho }=k$ and $[[{\alpha }_i+k{]]}_{\rho }=\rho (i)+k$. Symbolic evaluation $[[a{]]}_{\sigma }$ replaces the variable in $a$ by its symbolic term and adds the constant.

Proof of Lemma 69.1 — Expression correspondence

Proof. For a constant, both sides are $k$. For $x+k$, Subtract the two expression equalities to obtain the guard case. ◻

For the input $4$, begin with ${\sigma }_0(x)={\sigma }_0(y)=0$. After input, ${\sigma }_1={\sigma }_0[x\mapsto {\alpha }_0]$. On the right branch, ${\sigma }_2={\sigma }_1[y\mapsto {\alpha }_0-1]$. With $\rho (0)=4$, its concrete instance has $s(x)=4$ and $s(y)=3$.

Paths and the symbolic machine

A path condition $\mathrm{\Phi }$ is a finite conjunction of symbolic difference atoms; the empty conjunction is $\mathrm{\top }$. Negation stays inside the language: over integers, $$\begin{array}{}\text{(}\mathsf{neg}\text{)}& \mathrm{\neg }(t-u\le k)\text{means}u-t\le -k-1.\end{array}$$ A symbolic state is $⟨c,\sigma ,\mathrm{\Phi },n⟩$. The transition relation ${⟶}_{\mathsf{s}}$ does not ask whether a newly extended condition is satisfiable. Consequently no solver result can delete a state during the semantic proof.

The characteristic rules are $$\frac{\phantom{X}}{⟨\mathbf{input}x,\sigma ,\mathrm{\Phi },n⟩{⟶}_{\mathsf{s}}⟨\mathbf{skip},\sigma [x\mapsto {\alpha }_n],\mathrm{\Phi },n+1⟩}\mathrm{S}-\mathrm{Input}$$ $$\frac{\phantom{X}}{⟨x:=a,\sigma ,\mathrm{\Phi },n⟩{⟶}_{\mathsf{s}}⟨\mathbf{skip},\sigma [x\mapsto [[a{]]}_{\sigma }],\mathrm{\Phi },n⟩}\mathrm{S}-\mathrm{Assign}$$ $$\frac{\phantom{X}}{⟨\mathbf{if}g\mathbf{then}{c}_1\mathbf{else}{c}_2,\sigma ,\mathrm{\Phi },n⟩{⟶}_{\mathsf{s}}⟨c_1,\sigma ,\mathrm{\Phi }\wedge [[g{]]}_{\sigma },n⟩}\mathrm{S}-\mathrm{If}-\mathrm{T}$$ $$\frac{\phantom{X}}{⟨\mathbf{if}g\mathbf{then}{c}_1\mathbf{else}{c}_2,\sigma ,\mathrm{\Phi },n⟩{⟶}_{\mathsf{s}}⟨c_2,\sigma ,\mathrm{\Phi }\wedge \mathrm{\neg }[[g{]]}_{\sigma },n⟩}\mathrm{S}-\mathrm{If}-\mathrm{F}.$$ An assertion has a successful successor with $\mathrm{\Phi }\wedge [g{]}_{\sigma }$ and a terminal obligation $\mathsf{fail}(\sigma ,\mathrm{\Phi }\wedge \mathrm{\neg }[g{]}_{\sigma },n)$. A while has the same two forks as an if: the true successor is $c;\mathbf{while}g\mathbf{do}c$, and the false successor is $\mathbf{skip}$. The sequencing rules are shared with the concrete machine. Thus a symbolic transition denotes a path choice, not a guess about satisfiability.

Full oracle agreement makes S-Input a genuine lock-step rule. For a terminal model, model-to-test constructs the oracle $I_{\rho }(j)=\rho (j)$; only its consumed prefix is emitted as the finite test.

Proof of Theorem 69.3 — One-step simulation

Proof. Proceed by cases on the displayed symbolic rule. S-Assign uses lemma 69.1; S-Input extends input agreement at the old cursor. In S-If-T, satisfaction of the new conjunct and expression correspondence make the concrete guard true, selecting the same branch. Equation (neg) gives the false case. Assertions use the same argument and agree on success or failure. Sequence and while cases rebuild the corresponding concrete rule. Store and path components not changed by a rule retain their representation clauses. ◻

Proof of Corollary 69.4 — Finite simulation and path soundness

Proof. Induct on the finite symbolic derivation. Path conditions grow by conjunction, so satisfaction of the final condition implies satisfaction of every prefix. Apply theorem 69.3 at the last step. ◻

For $\mathsf{Fork}$, the four terminal obligations are The models $-2,1,4$ cover the first, third, and fourth rows. The second row is infeasible.

Proof of Theorem 69.5 — Loop-free finite-path coverage

Proof. Induct on the concrete derivation. Deterministic concrete guard evaluation selects exactly one of the two symbolic successors, and lemma 69.1 proves that its added atom is satisfied. Assignment, input, assertion, and sequence follow their matching rules. Without while, each successor contains a proper command subterm after the finite administrative sequence steps, so the finitely branching tree is finite. ◻

A certificate boundary for difference logic

Normalize a difference atom to $u-v\le k$, allowing a distinguished zero symbol $0$. Its graph edge is $v\stackrel{k}{\to }u$. A certificate is a list of existing edge indices that forms a directed cycle. The trusted checker verifies incidence, closure, and a strictly negative sum.

Proof of Lemma 69.6 — Negative-cycle certificate soundness

Proof. Let the checked cycle be $v_0\stackrel{k_0}{\to }{v}_1\cdots \stackrel{k_{r-1}}{\to }{v}_r=v_0$. Satisfaction gives $\rho (v_{i+1})-\rho (v_i)\le k_i$. Sum the inequalities: a contradiction. This proof uses only the checker facts, not the algorithm that proposed the edge list. ◻

The infeasible left-failure condition contains ${\alpha }_0-0\le 0$ and $0-{\alpha }_0\le -2$. Their two graph edges form a cycle of weight $-2$, so the checker may prune it. A zero-weight cycle is not a certificate.

Proof of Theorem 69.7 — Certificate-checked pruning preserves coverage

Proof. The leaf representing a concrete execution has a satisfying valuation by the coverage induction. By lemma 69.6, no prefix of that leaf can carry an accepted certificate. Hence the exploration never prunes the representing branch. ◻

Satisfiability evidence has the opposite shape. A proposed integer map is accepted only after evaluating every atom. It then determines the consumed input prefix, and the concrete machine is replayed deterministically.

Proof of Theorem 69.8 — Model-to-test correctness

Proof. The model check establishes the satisfaction premise of corollary 69.4. That corollary produces the concrete execution. The replay check independently compares every branch and the terminal assertion, so a malformed trace or an unrelated model cannot be reported as the test for this path. ◻

An adapter result therefore has three trusted interpretations: King introduced symbolic execution as a program-testing method; the modern substitution and path-simulation pattern appears explicitly in the rules and correctness/completeness theorems of de Boer and Bonsangue [Kin76, dBB21]. WiSE mechanizes a richer reachability connection in Coq and separates soundness from the exhaustiveness assumptions of bug search [CS23]. Our theorem is the local SymImp-DL proof, not a transfer of either richer result.

Explosion, subsumption, and guarded merging

A sequence of $m$ independent conditionals has $2^m$ syntactic leaves. In conjunctive SymImp-DL we may safely discard a state $⟨c,\sigma ,{\mathrm{\Phi }}_2,n⟩$ when a retained state has the same $c,\sigma ,n$ and a checked implication ${\mathrm{\Phi }}_2{\vDash }_{\mathsf{DL}}{\mathrm{\Phi }}_1$: every store represented by the discarded state is already represented by the first. For difference logic, each demanded implication may be checked by adding the complement of its consequent atom and accepting a negative-cycle certificate.

Proof of Proposition 69.9 — Subsumption soundness

Proof. If $\rho {\vDash }_{\mathsf{DL}}{\mathrm{\Phi }}_2$, the checked implication gives $\rho {\vDash }_{\mathsf{DL}}{\mathrm{\Phi }}_1$. Equality of command, store, and cursor leaves every other clause of definition 69.2 unchanged. ◻

General merging does not fit that representation. The separate extension SymImp-DL$\vee$ admits Boolean path formulas and guarded terms $\mathsf{ite}(B,t_1,t_2)$. Two states at the same command and cursor merge as $$({\sigma }_1,{\mathrm{\Phi }}_1),({\sigma }_2,{\mathrm{\Phi }}_2){⟼}_{\vee }(x\mapsto \mathsf{ite}({\mathrm{\Phi }}_1,{\sigma }_1(x),{\sigma }_2(x)),{\mathrm{\Phi }}_1\vee {\mathrm{\Phi }}_2).$$

Proof of Proposition 69.10 — Guarded-merge representation

Proof. Evaluate the disjunction. If ${\mathrm{\Phi }}_1$ holds, disjointness excludes ${\mathrm{\Phi }}_2$, and every guarded store component evaluates to ${\sigma }_1(x)$. Otherwise satisfaction forces ${\mathrm{\Phi }}_2$, and it evaluates to ${\sigma }_2(x)$. Conversely, a valuation represented by either input satisfies the disjunction and the corresponding guard. ◻

The unguarded merge ${\mathrm{\Phi }}_1\vee {\mathrm{\Phi }}_2$ with a single arbitrarily selected store is unsound. From branches $x=0,y=0$ and $x=1,y=1$, selecting the first store under the disjunction admits input $x=1$ paired with $y=0$, a state in neither branch. No simulation or coverage theorem transfers from SymImp-DL to the extension until its guarded-expression cases are proved.

Loops and concolic guidance

Loops require three different contracts.

1. A depth bound explores only paths with at most that many loop unfoldings. It is path fuel, not evidence that the source loop terminates.

2. A user invariant $J$ is checked by initiation $\mathrm{\Phi }\Rightarrow J$, preservation $J\wedge g\Rightarrow \mathsf{wp}(c,J)$, and exit $J\wedge \mathrm{\neg }g\Rightarrow Q$. The conclusion is the stated partial-correctness postcondition $Q$, not complete test generation.

3. Unbounded exploration retains every generated path but has no search termination claim.

Concolic execution carries a concrete oracle beside the symbolic state. It follows the concrete branch while recording the symbolic atom. To schedule an alternate, keep the prefix before branch $j$, negate its atom, obtain checked model ${\rho }^{\prime }$, and replay from the beginning.

Proof of Theorem 69.11 — Concolic alternate-input justification

Proof. Apply expression correspondence at every prefix guard. Each has the recorded truth value. At $j$, equation (neg) gives the opposite truth value. Determinism fixes the replayed control path through that point. ◻

This is the feedback loop used by DART and CUTE [GKS05, SMA05]. Complete branch coverage follows only when the chosen exploration schedule is fair over the finite loop-free tree and the constraint procedure eventually returns a checked model or certificate for every supported condition. Timeouts and unknown invalidate completeness, not soundness.

From paths to intervals

There is an explicit abstraction to the interval domain of chapter 25. For a finite family of symbolic states at one command, concretize each by its path condition and symbolic store, take their union, then take the least interval box containing that union. For $\mathsf{Fork}$, the two post-branch symbolic relations are $$x\le 0\wedge y=x+1,x\ge 1\wedge y=x-1.$$ Their interval hull is $x,y\in [-\mathrm{\infty },+\mathrm{\infty }]$. The implication $x\ge 4\Rightarrow y\ge 3$, which isolates the failed assertion, is lost. The abstraction is sound because every represented store lies in its hull; it is deliberately incomplete because the hull contains stores satisfying neither relation. Symbolic execution and abstract interpretation are related by this map, not identified as implementation variants.

Chapter seminar

The Kappa companion at artifacts/ch69-symimp-dl/ implements the finite SymImp-DL command and path AST, a fuel-bounded symbolic work-list explorer, concrete replay, model checking, and certificate-edge incidence plus negative-cycle checking. Its Agda companion states the store-representation relation and proves expression correspondence for the copy-plus-constant fragment; appendix E records the mechanized boundary.

The proved core ends at conjunctive difference constraints, finite symbolic derivations, local certificate/model checking, and deterministic replay. General SMT completeness, unrestricted-loop coverage, separation-logic heaps, concurrency, quantified theories, and floating point require new semantics or solver theorems. Symbolic execution produces paths and tests; it does not by itself produce a residual executable program.