For those hearing about SAT solvers for the first time, its worth mentioning that they are the basic component of hardware (and software) formal verification systems.
This is probably the largest practical application domain, which also drives most of the academic development.
>they are the basic component of hardware (and software) formal verification systems.
They are _a_ component. It's quite possible to perform formal verification without them, for instance the CompCert verified C compiler, or the DeepSpec end-to-end verification project: https://deepspec.org/main. SAT solvers generally have poor support for constructive logic, the kind of logic used in theorem provers based on dependent types like Coq. Systems based on classical logic like HOL integrate better with SAT solvers, but the lack of dependent types makes a lot of things much cumbersome to prove, especially if one wants proofs that can be extracted to programs.
> SAT solvers generally have poor support for constructive logic, the kind of logic used in theorem provers based on dependent types like Coq.
Arguably, this is no longer the case. FStar [1] has dependent types, monadic effects, refinement types and a weakest precondition calculus (i.e. a richer type system than Coq) and uses the Z3 SMT solver to discharge many proof obligations. I've been using FStar recently and it works surprisingly well.
There are other methods, no doubt. But last time I was involved with the field, software verification was still an experimental thing, that kind of worked in some niche cases, while SAT based verification was applied to every new arithmetic hardware design. Not to disregard other methods, but I'd say SAT still qualifies as being _the_ component.
Agreed! I started verifying stuff with different tools as part of my PhD and it is really not that hard to grasp the basic concepts. It becomes more complex the deeper you delve in the internals, but I think it would be great if more people verified part of their code in addition to testing it.
Personally, I started with CBMC [1]: it is quite a staple in the field and their documentation is very clear. Basically, it translates a C program (decorated with assumptions and properties to verify) into a SAT formula: if the formula is satisfiable, a property can be violated (and you even get a program trace that shows exactly how that happens).
This is probably the largest practical application domain, which also drives most of the academic development.