Very nice, thank you for sharing this!<p>Symbolic execution is also known as <i>abstract interpretation</i>. The program is being interpreted, with concrete values <i>abstracted away</i>, generalized to symbolic elements that often denote several or even infinitely many <i>concrete</i> values.<p>Logic programming languages like Prolog are especially amenable to abstract interpretation, since we can <i>absorb</i> the Prolog system's built-in binding environment for variables, and simply plug in different values for the existing variables. We only have to <i>reify</i> unification, i.e., implement it within the language with suitable semantics.<p>An impressive application of this idea is contained in the paper <i>Meta-circular Abstract Interpretation in Prolog</i> by Michael Codish and Harald Søndergaard:<p><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137.3604" rel="nofollow">http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.137....</a><p>As one of the examples, the authors show how abstract interpretation over the abstract parity domain {zero, one, even, odd} can be used to derive non-trivial facts about the Ackermann function.<p>In particular, they deduce that <i>Ackermann(i,j)</i> is odd and greater than 1 for all <i>i</i> greater than 1, by taking a Prolog implementation of the Ackermann function, and interpreting it with these abstract domain elements instead of all concrete values (which would not terminate, since there are infinitely many concrete values). This is computed by fixpoint computation, determining the deductive closure of the relation.