Introduction to Symbolic Execution¶

Grackle uses symbolic execution to generate formal models from programs. Symbolic execution differs from ordinary execution in that in ordinary execution the program variables are bound to specific values such as the number 3, while in symbolic execution program variables may be bound to mathematical formulas. The mathematical formula may be a concrete value, such as 3, but it may also be an expression, such as x + 2y, where x and y are variables representing arbitrary values.

When using Grackle, one can construct new symbolic variables, execute code to build up symbolic expressions, generate a proposition that describes a property of interest, such as x > y + 2, and then invoke a constraint solver to find values that can be assigned to x and y for the proposition to hold.

In this section, we describe some of those concepts and how they are implemented in Grackle so that more advanced users can get even more benefit out of Grackle, and use it to solve harder problems.