Model checking employs abstract interpretation, so it's similar to static analysis. I hesitate to use the latter term, because it's often used to describe how l

Model checking employs abstract interpretation, so it's similar to static analysis. I hesitate to use the latter term, because it's often used to describe how linting works. This is significantly more advanced. The model checker translates an abstract model of execution for the code into an SMT solver, and uses this to find counter-examples. The SMT solver works backward from failure cases to discover a combination of inputs or program state that can cause any one of these failure cases. This traces memory, data flow, and control flow. It's actually a pretty neat thing. It doesn't require existing test coverage or anything at runtime to work.