| Distinguishing Features of Sub-area | Type System | Program Analysis | Theorem Prover | Model Checking |
| Program Code | Applicable | Applicable | Not applicable | Not applicable |
| Model (Abstraction) | Not applicable | Control-Flow Graph (CFG) | Model construction | Finite-State Machine (FSM) |
| Type Checking | Applicable | Not applicable | Not applicable | Not applicable |
| Invariant Checking | Not applicable | Applicable | Applicable | Applicable |
| Functional Correctness | Not applicable | Applicable | Not applicable | Not applicable |
| Temporal Properties | Not applicable | Not applicable | Not applicable | Applicable |
| Symbolic Execution | Not applicable | Not applicable | Applicable | Applicable |
| Precision | Not applicable | Not applicable | Applicable | Applicable |
| Scalability | Not applicable | Applicable | Applicable | Not applicable |
| Exhaustive | Not applicable | Applicable | Applicable | Applicable |
| Efficiency | Not applicable | Applicable | Not applicable | Not applicable |
| Undesirable State | Type error | Spurious error | Invalid query | Spurious/coarse abstraction |
| Counter-example | Not applicable | Not applicable | Applicable | Applicable |
| Refinement | Not applicable | Not applicable | Applicable | Applicable |
| Proposed Properties | Not applicable | Applicable | Not applicable | Applicable |
| Inner Properties | Applicable | Not applicable | Applicable | Not applicable |