What are the differences between symbolic execution and SAT solvers?

Question

My understanding is that symbolic execution only deals with specific paths and bad patterns, while SAT solvers, or satisfiability modulo theories in general, provide a much more robust analysis of the program.

Could someone validate the statement above and (briefly) explain the differences between these two formal verification methodologies?

Answer 1

TL;DR: They differ in their basic input and output. SAT and SMT solvers don't know what programs are; they are tools that answer yes or no questions about mathematical formulas. Symbolic execution, on the other hand, is a method of analyzing programs. Symbolic execution usually relies on SAT and SMT solvers, but not the other way around.

---

SAT and SMT solvers don't directly have anything to do with programs. Instead, a SAT or SMT solver takes as input a mathematically described "formula", and answers, roughly, whether it is true or false. (Often a third option is allowed, unknown, for cases where the solver is unable to figure out an answer.)

For example, a possible input to a SAT solver is (a and not b) or (not a and c). That is, it is a mathematical formula, where a, b, and c here are Boolean (0 or 1) constants. The SAT solver is supposed to decide if it is possible for the formula to be true, by choosing values of a, b, and c. SMT solvers are similar, but a, b, and c would be replaced by more complex formulas using integers, strings, functions, etc., for example x + 3 = y^2.

---

Symbolic execution is a fancy way of running a program, but not how the program was intended to be run. Instead, the program is run using so-called "symbolic" values, which are kind of like placeholders. For an example of what that means, suppose I have a function like f(x) = if x > 0 then 1 else 0. Now, normally, I would run the program by inputting, say, 3, and get f(3) = 1, since 3 is greater than 0. With symbolic execution, I run the program by inputting a placeholder variable, input, and I evaluate the program to get two cases: either input > 0 and answer = 1 or input <= 0 and answer = 0. This may seem useless, but it ends up being a powerful way of analyzing programs.

---

The connection between the two is that symbolic execution often relies on SMT solvers during execution, to figure out if a certain path is actually possible, or if it should be discarded. For example, an SMT solver could be used to determine if input <= 0 and answer = 0 is possible (the answer is yes, for example if input = 0). In this way, SMT is kind of the "driving force" behind what makes symbolic execution feasible.