• README ⤓ .txt 2026-10-22T165042.936 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-10-22T165042.936 000000000000944
  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-08-20T080700.000 000000000058440
  Jean-Raymond Abrial, developed through the 1980s and set out in The B-Book: Assigning Programs to Meanings (Cambridge, 1996). Descends from Abrial's earlier Z notation but replaces Z's schema calculus with a calculus of generalised substitutions, giving specification and code a single semantics. Industrialized as Atelier B. Superseded for reactive systems by Event-B, which keeps the set theory and discards the operation-call model.
• BAN Logic ⤓ .md 2026-10-22T225449.000 000000000080488
  Michael Burrows, Martín Abadi, and Roger Needham, "A logic of authentication". The publication trail: DEC SRC Research Report 39 (February 1989, revised February 1990); Proceedings of the Royal Society of London A 426 (1989), 233–271; SOSP 1989, 1–13; ACM Transactions on Computer Systems 8(1) (1990), 18–36. Its analyses found weaknesses in published protocols, X.509 and the Andrew handshake among them.
• Bounded Model Checking ⤓ .md 2026-10-22T090936.000 000000000036632
  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-10-22T180154.561 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-08-20T065751.000 000000000042696
  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-10-22T091825.000 000000000032912
  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 checks a timed-CTL subset over timed automata.
• Concurrent Program Logic ⤓ .md 2026-10-22T090936.000 000000000035304
  Owicki and Gries (1976) for shared variables: parallel composition rule, interference freedom, auxiliary variables. Lamport (1977) gave a related shared-variable system. Apt, Francez, and de Roever (1980) gave the counterpart for CSP message passing, where a cooperation test replaces the interference-freedom test. Foundation for shared-memory verification.
• Concurrent Separation Logic ⤓ .md 2026-10-22T180154.561 000000000000976
  Peter O'Hearn extended separation logic to concurrency (2004, 2007). Stephen Brookes provided semantics. 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-10-22T084914.000 000000000035904
  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-08-20T083225.000 000000000044784
  Vaughan Pratt introduced dynamic logic in 1976 ("Semantical considerations on Floyd–Hoare logic"), reading programs as modalities. Fischer and Ladner isolated the propositional fragment PDL, combining modal logic with regular expressions over programs, and settled its complexity (1977, 1979). David Harel developed the first-order theory (1979). Foundational for program verification and reasoning about actions.
• Event-B ⤓ .md 2026-08-20T081411.000 000000000053712
  Jean-Raymond Abrial, developed through the EU RODIN (2004–2007) and DEPLOY (2008–2012) projects and set out in Modeling in Event-B: System and Software Engineering (Cambridge, 2010). Retains the B Method's typed set theory and drops its Generalised Substitution Language along with the operation-call model. Foundation of the Rodin platform.
• Game Logic ⤓ .md 2026-08-20T075111.000 000000000040168
  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-10-22T180154.561 000000000000896
  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; Atkey and McBride (2013) added clocks for productivity.
• Hoare Logic ⤓ .md 2026-08-20T063156.000 000000000043656
  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.
• Hybrid Automata ⤓ .md 2026-10-22T225319.000 000000000067856
  Rajeev Alur, Costas Courcoubetis, Thomas Henzinger, and Pei-Hsin Ho, "Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems" (Hybrid Systems, LNCS 736, 1993, 209–229), defined the model; the nine-author sequel with Nicolas Halbwachs, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine, "The algorithmic analysis of hybrid systems" (Theoretical Computer Science 138, 1995, 3–34), fixed the linear class and its symbolic analysis. Thomas Henzinger, "The theory of hybrid automata" (LICS 1996, 278–292), is the consolidated statement. The decidability frontier is Thomas Henzinger, Peter Kopke, Anuj Puri, and Pravin Varaiya, "What's decidable about hybrid automata?" (STOC 1995, 373–382; Journal of Computer and System Sciences 57, 1998, 94–124), and its o-minimal side is Gerardo Lafferriere, George Pappas, and Shankar Sastry, "O-minimal hybrid systems" (Mathematics of Control, Signals, and Systems 13, 2000, 1–21).
• Hyper Hoare Logic ⤓ .md 2026-08-20T070020.000 000000000044832
  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-08-20T065613.000 000000000043104
  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-10-22T085025.000 000000000051264
  Raad, Berdine, Dang, Dreyer, O'Hearn, Villard, "Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic" (CAV 2020). Combines O'Hearn's under-approximate triples with the frame rule. True positives: real bugs. Extended to concurrency by Raad, Berdine, Dreyer, O'Hearn (2022). Foundation for bug-finding tools.
• Interpolation-Based Verification ⤓ .md 2026-08-20T072252.000 000000000037168
  McMillan (2003). Craig interpolants from UNSAT proofs. Approximate forward/backward reachability. Completeness without state explosion. Foundation for modern IC3/PDR.
• Iris Logic ⤓ .md 2026-10-22T090022.000 000000000040440
  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-10-22T090631.000 000000000037592
  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-10-22T091817.000 000000000032096
  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).
• Modal Mu-Calculus ⤓ .md 2026-08-20T030722.000 000000000049264
  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-10-22T165042.936 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-08-20T065729.000 000000000050208
  Noam Zilberstein, Derek Dreyer, and Alexandra Silva, "Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning" (OOPSLA 2023; PACMPL 7(OOPSLA1):522–550; arXiv:2303.03111). Continued in outcome separation logic (Zilberstein, Saliling, Silva 2024), demonic outcome logic (Zilberstein, Kozen, Silva, Tassarotti 2025), and a general metatheory for branching effects (Zilberstein, TOPLAS 2025).
• Owicki-Gries Logic ⤓ .md 2026-10-22T180154.561 000000000000904
  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-08-20T074348.000 000000000038552
  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-08-20T072117.000 000000000039968
  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-10-22T090936.000 000000000041552
  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-10-22T085236.000 000000000043200
  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.
• Quantified Boolean Formulas ⤓ .md 2026-10-22T180154.561 000000000000976
  Larry J. Stockmeyer and Albert R. Meyer, "Word Problems Requiring Exponential Time: Preliminary Report" (Proceedings of the 5th ACM Symposium on Theory of Computing, 1973, 1–9), proved the truth problem for quantified Boolean formulas PSPACE-complete; the encoding of a long computation by recursive halving follows the construction of Savitch's theorem (1970). Stockmeyer, "The Polynomial-Time Hierarchy" (Theoretical Computer Science 3, 1976, 1–22), fixed the bounded-alternation levels: with k alternating quantifier blocks beginning existentially, truth is Σᵖₖ-complete (Celia Wrathall, 1977, for CNF and DNF matrices). Q-resolution is from Hans Kleine Büning, Marek Karpinski and Andreas Flögel, "Resolution for Quantified Boolean Formulas" (Information and Computation 117, 1995, 12–18); the dependency-quantified extension descends from Gary L. Peterson and John H. Reif, "Multiple-Person Alternation" (FOCS 1979), completed in Peterson, Reif and Azhar (2001).
• Quantitative Separation Logic ⤓ .md 2026-10-22T090023.000 000000000052784
  Batz, Kaminski, Katoen, Matheja, and Noll, "Quantitative separation logic: a logic for reasoning about probabilistic pointer programs" (POPL 2019; arXiv:1802.10467). It joins two lines that had stayed apart: Ishtiaq, O'Hearn, and Reynolds' separation logic for heap manipulation, and Kozen's and McIver and Morgan's weakest preexpectations for probabilistic programs. Extended to concurrency by Fesefeldt, Katoen, and Noll (CONCUR 2022). Not to be confused with Atkey's quantitative type theory, nor with his amortised resource analysis in separation logic — different systems with adjacent names.
• Reachability Logic ⤓ .md 2026-08-20T070042.000 000000000041600
  Roșu et al. (2012). Language-independent program verification. Reachability rules: φ ⇒ ψ. Derived from operational semantics. Foundation for K framework verification.
• Refinement Calculus ⤓ .md 2026-08-20T065447.000 000000000041680
  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-08-20T065356.000 000000000039408
  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-08-20T073338.000 000000000038248
  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-08-20T064959.000 000000000050480
  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-08-20T071852.000 000000000036952
  King (1976). Execute with symbolic values instead of concrete. Accumulate path conditions. Explore all paths systematically. Foundation for testing and verification.
• Timed Automata ⤓ .md 2026-10-22T180154.561 000000000000872
  Rajeev Alur and David Dill, "Automata for modeling real-time systems" (ICALP 1990), in journal form "A theory of timed automata" (Theoretical Computer Science 126, 1994, 183–235): finite automata over infinite words augmented with real-valued clocks, guards comparing clocks to constants, and resets. The companion logic is TCTL: Rajeev Alur, Costas Courcoubetis, and David Dill, "Model-checking in dense real-time" (Information and Computation 104, 1993, 2–34). David Dill, "Timing assumptions and verification of finite-state concurrent systems" (CAV 1989), supplied the zone and difference-bound-matrix machinery the implementations run on.
• TLA+ ⤓ .md 2026-10-22T090025.000 000000000040480
  Leslie Lamport (1990s). Concurrent systems. Actions as formulas. Stuttering invariance. Foundation of distributed systems verification.
• Weakest Precondition Calculus ⤓ .md 2026-08-20T064856.000 000000000049112
  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-10-22T165042.936 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).