• README ⤓ .txt 2026-07-17T121634.146 000000000000816
  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.
• Abstract Interpretation ⤓ .md 2026-07-15T060045.000 000000000023544
  Cousot and Cousot introduced abstract interpretation (1977). Framework for sound approximation of program semantics. Abstract domains capture properties of interest. Galois connections formalize soundness. Foundation for static analysis tools (Astrée, Polyspace, Infer).
• B Method ⤓ .md 2026-07-15T085851.000 000000000013424
  Jean-Raymond Abrial (1980s). Abstract machines. Refinement-based. Set-theoretic specification. Foundation of Event-B.
• Bounded Model Checking ⤓ .md 2026-07-15T065018.000 000000000015544
  Biere, Cimatti, Clarke, Zhu (1999). Unroll transition relation k times. SAT encoding of bounded reachability. No state explosion for bounded depth. Foundation for industrial verification.
• Buchi Automata ⤓ .md 2026-07-17T120407.600 000000000000872
  J. Richard Büchi, "On a decision method in restricted second order arithmetic" (1962), which introduced ω-automata to prove S1S decidable; Rabin (1969) extended it to trees and S2S; McNaughton (1966) gave the determinization. Vardi and Wolper's "An automata-theoretic approach to automatic program verification" (1986) turned the theorem into the technology every model checker runs on.
• Bunched Implications ⤓ .md 2026-07-15T055813.000 000000000022048
  O'Hearn and Pym introduced bunched implications (BI, 1999). Combines intuitionistic logic with linear/resource logic. Two conjunctions: additive (∧) and multiplicative (*). Foundation for separation logic. Substructural logic with resource sensitivity.
• Computation Tree Logic ⤓ .md 2026-07-15T060903.000 000000000020224
  Clarke and Emerson introduced CTL (1981). Branching time: tree of possible futures. Path quantifiers + temporal operators. Foundation for symbolic model checking. CTL* combines CTL and LTL. Tools: SMV, NuSMV, UPPAAL.
• Concurrent Program Logic ⤓ .md 2026-07-15T071625.000 000000000016624
  Apt, Francez, de Roever (1980). Extended Hoare logic for concurrency. Parallel composition rule. Non-interference. Foundation for shared-memory verification.
• Concurrent Separation Logic ⤓ .md 2026-07-15T055424.000 000000000028320
  Peter O'Hearn extended separation logic to concurrency (2004, 2007). Stephen Brookes provided semantics. The key insight: separating conjunction extends to thread separation — disjoint resources enable parallel composition. Foundation for modern concurrent program verification. Evolved into Iris, VST, and other frameworks.
• CTL Star ⤓ .md 2026-07-17T120407.600 000000000000736
  Emerson and Halpern (1986), "Sometimes and Not Never Revisited." The logic that subsumes both CTL and LTL by freely combining path quantifiers with linear temporal operators, resolving the expressiveness dispute between branching- and linear-time schools.
• Dynamic Logic ⤓ .md 2026-07-15T052745.000 000000000026680
  Vaughan Pratt introduced Propositional Dynamic Logic (PDL) in 1976, combining modal logic with regular expressions over programs. David Harel extended it to first-order (1979). Fischer and Ladner analyzed complexity. Foundational for program verification and reasoning about actions.
• Event-B ⤓ .md 2026-07-15T085857.000 000000000012160
  Jean-Raymond Abrial (2000s). Evolution of B. Event-driven. Reactive systems. Foundation of Rodin platform.
• Game Logic ⤓ .md 2026-07-15T054808.000 000000000025352
  Rohit Parikh introduced propositional game logic (1985). Builds on dynamic logic, adding game-theoretic operations. Models strategic interaction where outcomes depend on choices of multiple agents. Connects logic, game theory, and verification. Extended by various researchers for different game-theoretic concepts.
• Guarded Recursion ⤓ .md 2026-07-16T001655.000 000000000034368
  Hiroshi Nakano, "A modality for recursion" (LICS 2000), which introduced the later modality ▷ and its fixed-point combinator; Appel, Melliès, Richards, and Vouillon's "very modal model" (2007) connected it to step-indexing; Birkedal, Møgelberg, Schwinghammer, and Støvring's topos of trees (2011) gave the canonical model; Clouston, Bizjak, Grathwohl, and Birkedal (2015) added clocks for productivity.
• Hoare Logic ⤓ .md 2026-07-15T053457.000 000000000027328
  C.A.R. Hoare introduced the axiomatic approach to program correctness (1969). Building on Floyd's work on flowcharts (1967). Foundation for formal program verification. Extended by many: weakest preconditions (Dijkstra), refinement calculus, separation logic. Turing Award 1980.
• Hyper Hoare Logic ⤓ .md 2026-07-15T061936.000 000000000020904
  Dardinier, Müller, and colleagues developed hyper Hoare logic (2020s). Reasons about hyperproperties: properties of sets of traces. Standard Hoare: single execution. Hyper: relationships between executions. Non-interference, observational determinism.
• Incorrectness Logic ⤓ .md 2026-07-15T055806.000 000000000024224
  Peter O'Hearn introduced incorrectness logic (2019). Dual to Hoare logic: reasons about presence of bugs rather than absence. "Under-approximate" rather than "over-approximate." Designed for bug-finding tools like Infer's Pulse. Connects to reverse Hoare logic and outcome logic.
• Incorrectness Separation Logic ⤓ .md 2026-07-15T071627.000 000000000016968
  Raad, Berdine, Dang, Dreyer, O'Hearn (2022). Under-approximate reasoning for bugs. True positives: real bugs. Separation for heap. Foundation for bug-finding tools.
• Interpolation-Based Verification ⤓ .md 2026-07-15T065023.000 000000000015488
  McMillan (2003). Craig interpolants from UNSAT proofs. Approximate forward/backward reachability. Completeness without state explosion. Foundation for modern IC3/PDR.
• Iris Logic ⤓ .md 2026-07-15T062338.000 000000000019552
  Jung, Krebbers, Jourdan, Bizjak, Birkedal, Dreyer developed Iris (2015-present). Higher-order concurrent separation logic in Coq. Unifies many verification techniques. Ghost state, invariants, protocols. State-of-the-art program verification framework.
• Linear Logic ⤓ .md 2026-07-15T071424.000 000000000018112
  Girard (1987). Resource-sensitive logic. Formulas as resources, used exactly once. Multiplicative/additive distinction. Foundation for concurrency, quantum, and programming language theory.
• Linear Temporal Logic ⤓ .md 2026-07-15T060902.000 000000000019448
  Pnueli introduced LTL for program verification (1977). Temporal operators over infinite sequences. Linear time: one future path. Foundation for model checking (Vardi, Wolper). Tools: SPIN, NuSMV, SPOT. Turing Award to Pnueli (1996).
• Mu-Calculus ⤓ .md 2026-07-17T120407.600 000000000000848
  Dana Scott and Jaco de Bakker used fixed points in program semantics (1969); Park (1969, 1976) on fixpoint induction. Dexter Kozen, "Results on the propositional μ-calculus" (1983), gave the system and its axiomatization; Walukiewicz (1995) proved completeness. The modal mu-calculus combines modal logic with fixed-point operators. Subsumes CTL, LTL, PDL in expressive power. Foundation for model checking algorithms (OBDD-based, game-based).
• Nelson-Oppen Combination ⤓ .md 2026-07-17T120407.600 000000000000952
  Greg Nelson and Derek Oppen, "Simplification by cooperating decision procedures" (ACM TOPLAS 1, 1979). Robert Shostak's alternative method (1984) covered a narrower class more efficiently and its original correctness proof was wrong — Rueß and Shankar (2001) gave the first correct version, and Shostak's method is now understood as an instance of Nelson–Oppen. Tinelli and Harandi (1996) gave the clean model-theoretic proof; Ghilardi (2004) extended the result to non-disjoint signatures under model-completeness conditions.
• Outcome Logic ⤓ .md 2026-07-15T061555.000 000000000019688
  Zilberstein and colleagues introduced Outcome Logic (2023). Unifies Hoare logic (over-approximate) and incorrectness logic (under-approximate). Both forward and backward reasoning. Hyperproperty reasoning about sets of traces. Modern framework for program verification.
• Owicki-Gries Logic ⤓ .md 2026-07-15T063457.000 000000000020328
  Owicki and Gries developed method (1976). Extends Hoare logic to parallel programs. Auxiliary variables for coordination. Non-interference: parallel threads don't invalidate each other's proofs. Foundation for concurrent verification.
• Parity Games ⤓ .md 2026-07-15T065146.000 000000000015248
  Emerson and Jutla (1991). Two-player infinite games on graphs. Parity condition on infinite plays. Decides μ-calculus satisfiability. Positional strategies suffice.
• Predicate Abstraction ⤓ .md 2026-07-15T065016.000 000000000015984
  Graf and Saïdi (1997). Abstract interpretation guided by predicates. Boolean programs from concrete programs. CEGAR loop. Foundation for SLAM, BLAST.
• Process Algebra ⤓ .md 2026-07-17T120407.600 000000000000872
  Robin Milner developed CCS (Calculus of Communicating Systems, 1980) and later the π-calculus (1992). Tony Hoare developed CSP (Communicating Sequential Processes, 1978, 1985). Jan Bergstra and Jan Willem Klop developed ACP (Algebra of Communicating Processes, 1984). These provide algebraic frameworks for concurrent and distributed systems.
• Proof Complexity ⤓ .md 2026-07-15T063113.000 000000000019744
  Cook and Reckhow initiated proof complexity (1979). Studies lengths of proofs in various systems. Lower bounds: some tautologies require long proofs. Connects to computational complexity (P vs NP). Propositional proof systems as central objects.
• Quantitative Separation Logic ⤓ .md 2026-07-17T120407.600 000000000000992
  Atkey introduced quantitative type theory (2018). Quantitative separation logic (QSL) by various authors. Tracks resource quantities, not just separation. Coefficients count resource usage. Foundation for linear/graded types.
• Reachability Logic ⤓ .md 2026-07-15T071529.000 000000000016672
  Roșu et al. (2012). Language-independent program verification. Reachability rules: φ ⇒ ψ. Derived from operational semantics. Foundation for K framework verification.
• Refinement Calculus ⤓ .md 2026-07-15T060047.000 000000000021696
  Back and Morgan developed refinement calculus (1980s). Extends Dijkstra's weakest preconditions to program derivation. Programs derived by stepwise refinement from specifications. Specification statements as primitive. Foundation for B-Method and Event-B.
• Rely-Guarantee Logic ⤓ .md 2026-07-15T062125.000 000000000020472
  Jones introduced Rely-Guarantee (1983). Compositional reasoning for concurrent programs. Rely: what environment may do. Guarantee: what this component does. Enables modular concurrent verification. Foundation for modern concurrent separation logic.
• Satisfiability Modulo Theories ⤓ .md 2026-07-15T060043.000 000000000022104
  SMT emerged from combining SAT solvers with decision procedures (2000s). Extends propositional satisfiability to first-order theories. Nelson-Oppen combination (1979). DPLL(T) architecture (Nieuwenhuis et al., 2006). Tools: Z3, CVC, Yices. Workhorse of modern verification.
• Separation Logic ⤓ .md 2026-07-15T053459.000 000000000028976
  John Reynolds (2000, 2002) and Peter O'Hearn (2001) extended Hoare logic with spatial connectives for heap reasoning. Builds on Burstall's work and bunched implications (O'Hearn & Pym). Enabled scalable verification of pointer-manipulating programs. Foundation for tools like Infer (Facebook).
• Symbolic Execution ⤓ .md 2026-07-15T065020.000 000000000014840
  King (1976). Execute with symbolic values instead of concrete. Accumulate path conditions. Explore all paths systematically. Foundation for testing and verification.
• TLA+ ⤓ .md 2026-07-17T120407.600 000000000000792
  Leslie Lamport (1990s). Concurrent systems. Actions as formulas. Stuttering invariance. Foundation of distributed systems verification.
• Weakest Precondition Calculus ⤓ .md 2026-07-17T120407.600 000000000000992
  Edsger Dijkstra (1975, "Guarded Commands, Nondeterminacy and Formal Derivation of Programs"; 1976 monograph). A predicate-transformer semantics giving each program a function on postconditions, turning correctness reasoning into predicate calculus and supporting the systematic derivation of programs from specifications.
• CRITERIA ⤓ .txt 2026-07-17T121634.146 000000000000832
  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).