.. _background_chapter:

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.

.. toctree::
   :maxdepth: 1

   background/symbolic_expressions
   background/execution_strategies
   background/constraint_solving
   background/architecture