Software model checking takes a program plus a property ("nothing is ever null-dereferenced", "this lock is always released") and asks: does there exist any input causing the property to fail? Bounded model checking unrolls the program k steps and encodes the question as a CNF formula — typically a few million 3-clauses for k = 50 in a real Java method. The JBMC, SPIN, and CBMC tool families all do this. The same template runs symbolic execution (KLEE, Coverity, GitHub CodeQL) and most of static analysis. When Microsoft's SLAM device-driver verifier was deployed in Windows, it caught crashes that traditional QA missed for years; it was, mechanically, a 3-SAT solver.
33
Verifying the JVM
Every time the Java verifier checks a class file, it is solving an instance of bounded model checking — which compiles to 3-SAT under the hood.