INCLUSION CRITERIA
An entry belongs in this subdivision if and only if it is a logic or calculus for proving program correctness or incorrectness, or an automated method for checking that a system meets a specification.
Required: At least one of the following:
- An assertion logic for program state, resource, or concurrency (Hoare, separation, rely-guarantee)
- A refinement or specification calculus relating programs to specifications (refinement calculus, B, TLA+)
- An automated verification method (model checking, SMT, symbolic execution, predicate abstraction)
Not sufficient: A tool that implements a logic rather than defining one — a verification infrastructure, an intermediate language, a proof assistant, a solver, or a framework. The entry belongs to the logic it implements: implicit dynamic frames rather than Viper, separation logic rather than the Verified Software Toolchain, CIC rather than Coq. A tool's name is not a system's name. A semantics of computation without a correctness judgment (Computation). A type system as such (Type). A bare temporal or dynamic modal logic absent the verification use (Modal).
Boundary: Temporal logics (LTL, CTL, mu-calculus) are cross-listed with Modal/Temporal; their use as checking targets places them here. Bunched implications is cross-listed with Structural/Linear. Parity games are cross-listed with Applications/Game.