PROGRAM VERIFICATION
Logics and calculi for proving programs correct or incorrect: assertion-based reasoning about state, resource, and concurrency, and the automated methods that check temporal and reachability properties of systems. The concern is correctness—establishing that a program meets or violates a specification.
Entries include the Hoare and separation family (Hoare logic, separation logic and its concurrent, quantitative, incorrectness, and hyper variants, Iris, implicit dynamic frames, bunched implications), the concurrency methods (rely-guarantee, Owicki-Gries, concurrent program logic), the refinement and specification languages (refinement calculus, B and Event-B, TLA+), the model-checking and decision methods (bounded model checking, CTL and LTL checking, the modal mu-calculus, satisfiability modulo theories, symbolic execution, predicate abstraction, interpolation-based verification, reachability and outcome logic), and the underlying complexity (proof complexity, parity games).