What are the differences between symbolic execution and SAT solvers?

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?

• What research have you done, and what resources have you read and what have you found so far?
– D.W.
May 29, 2020 at 3:12
• I'm not an expert in this field. Researching formal verification would've taken me weeks before I could come up with a mental model explainable to a 5-year old. May 29, 2020 at 9:31

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.