Program model checking refers to the application of model-checking techniques to software systems, and in particular to the final implementation where the code itself is the target of the analysis (Figure shown below). It can be effective at uncovering critical software defects that are hard to find using approaches such as traditional testing.
