| % formal/sat.tex |
| % SPDX-License-Identifier: CC-BY-SA-3.0 |
| |
| \section{SAT Solvers} |
| \label{sec:formal:SAT Solvers} |
| |
| Any finite program with bounded loops and recursion can be converted |
| into a logic expression, which might express that program's assertions |
| in terms of its inputs. |
| Given such a logic expression, it would be quite interesting to know |
| whether any possible combinations of inputs could result in one of |
| the assertions triggering. |
| If the inputs are expressed as combinations of boolean variables, |
| this is simply SAT, also known as the satisfiability problem. |
| SAT solvers are heavily used in verification of hardware, which has |
| motivated great advances. |
| A world-class early 1990s SAT solver might be able to handle a logic |
| expression with 100 distinct boolean variables, but by the early 2010s |
| million-variable SAT solvers were readily |
| available~\cite{Kroening:2008:DPA:1391237}. |
| |
| In addition, front-end programs for SAT solvers can automatically translate |
| C code into logic expressions, taking assertions into account and generating |
| assertions for error conditions such as array-bounds errors. |
| One example is the C bounded model checker, or \co{cbmc}, which is |
| available as part of many Linux distributions. |
| This tool is quite easy to use, with \co{cbmc test.c} sufficing to |
| validate \path{test.c}. |
| This ease of use is exceedingly important because it opens the door |
| to formal verification being incorporated into regression-testing |
| frameworks. |
| In contrast, the traditional tools that require non-trivial translation |
| to a special-purpose language are confined to design-time verification. |
| |
| More recently, SAT solvers have appeared that handle parallel code. |
| These solvers operate by converting the input code into single static |
| assignment (SSA) form, then generating all permitted access orders. |
| This approach seems promising, but it remains to be seen how well |
| it works in practice. |
| For example, it is not clear what types and sizes of programs this |
| technique handles. |
| However, there is some reason to hope that SAT solvers will be useful |
| for verifying parallel code. |
