See also: - Dein, ["Professional Programming"](https://github.com/charlax/professional-programming) - ["Computer-Aided Reasoning for Software"](https://courses.cs.washington.edu/courses/csep590b/26sp/library/) * Black (ed.), [Dictionary of Algorithms and Data Structures](https://xlinux.nist.gov/dads/) * [Open Logic Project](https://builds.openlogicproject.org) * [ ] Abelson and Sussman (1996), *Structure and Interpretation of Computer Programs* - [ ] Bornholt et al. (2021), ["Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3"](https://dl.acm.org/doi/10.1145/3477132.3483540) * [ ] Bradley and Manna (2007), *The Calculus of Computation* * [ ] Chlipala, [*Formal Reasoning about Programs*](http://adam.chlipala.net/frap/) * [ ] ["Formal Reasoning about Programs"](https://frap.csail.mit.edu/main) (MIT, spring 2023) * [ ] ["Principles of Programming Languages"](https://sites.google.com/cs.washington.edu/cse-505-18au) (University of Washington, fall 2018) * [ ] Chulipala (2022), *Certified Programming with Dependent Types* * [ ] Delaët et al. (2022), ["Turning Catala into a Proof Platform for the Law"](https://inria.hal.science/hal-03447072/) * [ ] Fichte et al. (2023), ["The Silent (R)evolution of SAT"](https://dl.acm.org/doi/pdf/10.1145/3560469) * [x] Floyd (1967), "Assigning Meanings to Programs" * [ ] Girard (1987), "Linear Logic" * [ ] Heuer et al. (2025), ["Functional State Machines in Rust: Typestate and Newtype Patterns"](https://dl.acm.org/doi/10.1145/3830438.3830958) * [x] Hoare (1969), "An Axiomatic Basis for Computer Programming" * [ ] Mora et al. (2023), ["Message Chains for Distributed System Verification"](https://dl.acm.org/doi/10.1145/3622876) * [ ] Naur (1985), ["Programming as Theory-Building"](https://gwern.net/doc/cs/algorithm/1985-naur.pdf) * [ ] Lamport (2026), *A Science of Concurrent Programs* * [ ] Lawsky (2017), ["A Logic for Statutes"](https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3088206) * [ ] Kun (2021), *A Programmer's Introduction to Mathematics* * [ ] Merigoux et al. (2021), ["Catala: A Programming Language for the Law"](https://inria.hal.science/hal-03159939) * [ ] Peirce (2002), *Types and Programming Languages* * [ ] Peirce et al., [*Software Foundations*](https://softwarefoundations.cis.upenn.edu): * [ ] *Logical Foundations* * [ ] *Programming Language Foundations* * [ ] *Verified Functional Algorithms* * [ ] Polakow and Pfenning (1999), ["Natural Deduction for Intuitionistic Non-Commutative Linear Logic"](https://www.cs.cmu.edu/~fp/papers/tlca99.pdf) * [ ] Reynolds (2002), "Separation Logic: A Logic for Shared Mutable Data Structures" * [ ] Scott and Strachey (1971), ["Towards a Mathematical Semantics for Computer Languages"](https://www.cs.cmu.edu/~crary/819-f09/Scott71.pdf) * [ ] Stonebreaker and Hellerstein (2005), ["What Goes Around Comes Around"](https://people.cs.umass.edu/~yanlei/courses/CS691LL-f06/papers/SH05.pdf) * [ ] Ulam (1990), [*Analogies between Analogies: The Mathematical Reports of S. M. Ulam and His Los Alamos Collaborators*](https://publishing.cdlib.org/ucpressebooks/view?docId=ft9g50091s&brand=ucpress) * [ ] Van Horn and Might (2010), ["Abstracting Abstract Machines"](https://dl.acm.org/doi/10.1145/1863543.1863553) * [ ] Wagner et al. (2025), ["From Linearity to Borrowing"](https://dl.acm.org/doi/10.1145/3764117) * [ ] Wayne (2024), [*Logic for Programmers*](https://leanpub.com/logic/) * [ ] Woos et al. (2016), ["Planning for Change in a Formal Verification of the Raft Consensus Protocol"](https://dl.acm.org/doi/abs/10.1145/2854065.2854081) * [ ] Yoshida and Gheri, ["A Very Gentle Introduction to Multiparty Session Types"](http://mrg.doc.ic.ac.uk/publications/a-very-gentle-introduction-to-multiparty-session-types/main.pdf) ### Code correctness/compliance - [ ] Kakarla et al. (2022), ["SCALE: Automatically Finding RFC Compliance Bugs in DNS Nameservers"](https://www.usenix.org/system/files/nsdi22-paper-kakarla.pdf) ## Data - [ ] Discoll et al. (1986), "Making Data Structures Persistent" - [ ] Shneiderman (1996), ["The Eyes Have It: A Task by Data Type Taxonomy for Information Visualizations"](https://www.cs.umd.edu/~ben/papers/Shneiderman1996eyes.pdf) - [ ] Wickham (2014), ["Tidy Data"](https://www.jstatsoft.org/article/view/v059i10/) ## Formal modeling, verification, and analysis With blurry overlap with [[cryptography, especially end-to-end encryption]]. - Spin, Simple Protocol Interpreter, Protocol Meta Language - The whole Tamarin lineage, per <https://iacr.org/submit/files/slides/2026/rwc/rwc2026/inv-1/inv-1_slides.pptx> * ["The Science of Deep Specification: Research Overview"](https://deepspec.org/page/Research/_) * [ ] Abadi and Cortier (2006), ["Deciding Knowledge in Security Protocols under Equational Theories"](https://dl.acm.org/doi/10.5555/1226644.1226646) * [ ] Appel (2015), ["Verification of a Cryptographic Primitive: SHA-256"](https://www.cs.princeton.edu/~appel/papers/verif-sha.pdf) * [x] Arquint et al. (2022), ["Sound Verification of Security Protocols: From Design to Interoperable Implementations"](https://arxiv.org/pdf/2212.04171) * [ ] Baanen et al. (2024), [*The Hitchhiker's Guide to Logical Verification*](https://lean-forward.github.io/hitchhikers-guide/2024/) * [ ] Backes et al. (2013), "AnoA: A Framework for Analyzing Anonymous Communication Protocols" * [ ] **Barbosa et al. (2019), ["SoK: Computer-Aided Cryptography"](https://eprint.iacr.org/2019/1393.pdf)** * [ ] Basin and Cremers (2014), ["Know Your Enemy: Compromising Adversaries in Protocol Analysis"](https://dl.acm.org/doi/abs/10.1145/2658996) * [ ] Basin et al. (2016), ["Modeling Human Errors in Security Protocols"](https://ieeexplore.ieee.org/document/7536385) - [ ] Bornholt et al. (2021), ["Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3"](https://dl.acm.org/doi/10.1145/3477132.3483540) - [x] Cassez (2001), ["Verification of the Incremental Merkle Tree Algorithm with Dafny"](https://franck44.github.io/publications/papers/merkle-fm-21.pdf) - [ ] Castillo-Perez and Garcia-Alfaro, (2009), "Evaluation of Two Privacy-Preserving Protocols for the DNS" * [ ] Celi et al. (2022), ["A Tale of Two Models: Formal Verification of KEMTLS via Tamarin"](https://eprint.iacr.org/2023/1933.pdf) * [ ] Chlipala et al. (2015), ["Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant"](https://dl.acm.org/doi/10.1145/2775051.2677006) * [ ] Chlipala (2018), ["The Surprising Security Benefits of End-to-End Formal Proofs"](https://cccblog.org/2018/06/13/the-surprising-security-benefits-of-end-to-end-formal-proofs/) * [ ] Cousot and Cousot, ["A Gentle Introduction to Formal Verification of Computer Systems by Abstract Interpretation"](https://www.di.ens.fr/~cousot/publications.www/CousotCousot-Marktoberdorf-2009.pdf) * [ ] Cremers et al. (2025), ["A Ladder of Cryptographic Problems to Illustrate Formal Verification"](https://github.com/charlie-j/fm-crypto-lib/blob/9c6c23045f1f16f2f0253c9a16aac83d9f427865/Notes/main.pdf) * [ ] Davis et al. (2020), ["eXtreme Modelling in Practice"](https://arxiv.org/abs/2006.00915) * [ ] Denning (1976), ["A Lattice Model of Secure Information Flow"](https://dl.acm.org/doi/10.1145/360051.360056) * [ ] Durgin et al. (2004), ["Multiset Rewriting and the Complexity of Bounded Security Protocols"](https://dl.acm.org/doi/10.5555/1017273.1017276) * [x] Gancher et al. (2023), ["OWL: Compositional Verification of Security Protocols via an Information-Flow Type System"](https://eprint.iacr.org/2023/473.pdf) * [x] Halevi (2005), ["A Plausible Approach to Computer-Aided Cryptographic Proofs"](https://eprint.iacr.org/2005/181.pdf) * [ ] Hui and Lowe (2001), "Fault-Preserving Simplifying Transformations for Security Protocols" * [ ] Jamner et al. (2025), ["Pyrosome: Verified Compilation for Modular Metatheory"](https://dl.acm.org/doi/10.1145/3763052) * [x] Jenny (2023), ["Verifying Go's Standard Library"](https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Adrian_Jenny_PW_Report.pdf) * [ ] Kobeissi et al. (2021), ["Verifpal: Cryptographic Protocol Analysis for the Real World"](https://iacr.org/submit/files/slides/2021/rwc/rwc2021/3/slides.pdf) * [ ] Le Blanc and Lam (2024), ["Surveying the Rust Verification Landscape"](https://arxiv.org/abs/2410.01981) * [ ] Larisch et al. (2024), ["Topaz: Declarative and Verifiable Authoritative DNS at CDN-Scale"](https://research.cloudflare.com/publications/Larisch2024/) * [ ] Lattuada et al. (2024), ["Verus: A Practical Foundation for Systems Verification"](https://dl.acm.org/doi/10.1145/3694715.3695952) * [ ] Lindell (2021), ["How To Simulate It: A Tutorial on the Simulation Proof Technique"](https://eprint.iacr.org/2016/046.pdf) * [ ] Lipp (2022), ["Mechanized Cryptographic Proofs of Protocols and their Link with Verified Implementations"](https://inria.hal.science/tel-03933719) * [x] Ma et al. (2025), ["SpecGen: Automated Generation of Formal Program Specifications via Large Language Models"](https://arxiv.org/abs/2401.08807) - [ ] Mora et al. (2023), ["Message Chains for Distributed System Verification"](https://dl.acm.org/doi/10.1145/3622876) * [ ] Murray and van Oorschot (2018), [“BP: Formal Proofs, the Fine Print and Side Effects”](https://people.scs.carleton.ca/~paulv/papers/secdev2018.pdf”) * [ ] Nipkow and Klein (2014), *Concrete Semantics* * [ ] Newcombe et al. (2015), ["How Amazon Uses Formal Methods"](https://dl.acm.org/doi/10.1145/2699417) * [ ] Protzenko et al. (2019), ["Formally Verified Cryptographic Web Applications in WebAssembly"](https://www.computer.org/csdl/proceedings-article/sp/2019/666000b256/1dlwheTvbEI) * [ ] Sammler et al. (2023), ["DimSum: A Decentralized Approach to Multi-language Semantics and Verification"](https://dl.acm.org/doi/10.1145/3571220) * [ ] Sergey et al. (2017), ["Programming and Proving with Distributed Protocols"](https://dl.acm.org/doi/abs/10.1145/3158116) * [ ] Singh et al. (2025), ["OwlC: Compiling Security Protocols to Verified, Secure, High-Performance Libraries"](https://eprint.iacr.org/2025/1092.pdf) * [ ] Sprenger et al. (2020), ["Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification"](https://dl.acm.org/doi/pdf/10.1145/3428220) * [ ] van Lamsweerde (2000), ["Formal Specification: A Roadmap"](hps://dl.acm.org/doi/10.1145/336512.336546) * [ ] Weisner (2022), ["Automated Translation of Tamarin Theories into I/O Specifications for Igloo"](https://www.research-collection.ethz.ch/entities/publication/70b92112-ca4a-4fba-9984-b6da72075e9d) * [ ] Wilcox et al. (2015), ["Verdi: A Framework for Implementing and Formally Verifying Distributed Systems"](https://dl.acm.org/doi/10.1145/2737924.2737958) * [ ] Wilcox et al. (2017), ["Programming Language Abstractions for Modularly Verified Distributed Systems"](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2017.19) ### Tamarin (needs deduplication) - Schmidt et al. (2012), "Automated Analysis of Diffie–Hellman Protocols and Advanced Security Properties" - Meier et al. (2013), "The Tamarin Prover for the Symbolic Analysis of Security Protocols" - Basin et al. (2014), "Modeling and Analyzing Security Protocols with Tamarin" - Cremers et al. (2014), "A Comprehensive Symbolic Analysis of TLS 1.3" - Basin et al. (2015), "Automated Symbolic Proofs of Observational Equivalence" - Dreier et al. (2015), "Automated Unbounded Verification of Stateful Security Protocols" - Dreier et al. (2017), "Automated Verification of Stateful Security Protocols with Global State" - Dreier et al. (2017), "Automated Analysis of Security Protocols with Global State" - Hirschi et al. (2018), "Deciding Protocol Security with Stateful Protocols" - Dreier et al. (2018), "Automated Unbounded Verification of Security Protocols with State" - Cremers et al. (2019), "Precise Symbolic Analysis of Diffie–Hellman Protocols" - Dreier et al. (2019), "Automated Analysis of Protocols with Algebraic Properties" - Hirschi et al. (2019), "Automated Reasoning about Protocols with Advanced Equational Theories" - Basin et al. (2020), "Symbolic Verification of Cryptographic Protocols with Global State" - Dreier et al. (2021), "Advanced Automated Reasoning for Stateful Security Protocols" - Sasse et al. (2022), "Symbolic Protocol Analysis for Complex Cryptographic Constructions" - Hirschi et al. (2023), "Constraint Solving Techniques for Symbolic Protocol Analysis" - Hirschi et al. (2023), "Efficient Symbolic Analysis of Cryptographic Protocols with Rich Equational Theories" - Hirschi et al. (2024), "Symbolic Analysis of Modern Cryptographic Protocols with Advanced Primitives" - Basin et al. (2025), "Compositional Security Analysis of Complex Cryptographic Protocols" - Blanchet (2001), "An Efficient Cryptographic Protocol Verifier Based on Prolog Rules" - Blanchet (2004), "Automatic Proof of Strong Secrecy for Security Protocols" - Blanchet (2016), "Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif" - Baudet (2005), "Deciding Security of Protocols against Off-Line Guessing Attacks" - Cheval et al. (2018), "Automated Verification of Equivalence Properties of Cryptographic Protocols" - Cortier et al. (2011), "A Survey of Symbolic Methods for Establishing Cryptographic Protocol Security" - Abadi and Blanchet (2005), "Analyzing Security Protocols with Secrecy Types and Logic Programs" - Abadi and Fournet (2001), "Mobile Values, New Names, and Secure Communication" - Delaune et al. (2009), "Symbolic Protocol Analysis with Equational Theories" - Linker (2026), ["Rule Variant Restrictions for the Tamarin Prover"](https://eprint.iacr.org/2026/230) - Linker et al. (2025), ["Looping for Good: Cyclic Proofs for Security Protocols"](https://doi.org/10.3929/ethz-c-000783356) - Cremers et al. (2024), ["Impossibility Results for Post-Compromise Security in Real-World Communication Systems"](https://eprint.iacr.org/2024/1886) - [ ] **Morio et al. (2026), ["A Sound Translation from Tamarin to ProVerif: Enabling Comparative Analysis"](https://arxiv.org/abs/2608.06315)** ### Hyperproperties and observational determinism For some reason, sorted by publication date rather than by author: - [ ] Lamport (1980), ["'Sometimes' Is Sometimes 'Not Never'"](https://hillelwayne.com/post/hyperproperties/) - [ ] Zdancewic and Myers (2003), ["Observational Determinism for Concurrent Program Security"](https://www.cs.cornell.edu/andru/papers/csfw03.pdf) - [ ] Barthe et al. (2004), ["Secure Information Flow by Self-Composition"](https://www.computer.org/csdl/proceedings-article/csfw/2004/21690100/12OmNxdm4uz) - [ ] Terauchi and Aiken (2005), ["Secure Information Flow as a Safety Problem"](https://theory.stanford.edu/~aiken/publications/papers/sas05b.pdf) - [ ] Huisman et al. (2006), ["A Temporal Logic Characterisation of Observational Determinism"](https://ieeexplore.ieee.org/document/1648704) - [ ] Smith (2007), ["Principles of Secure Information Flow Analysis"](https://www.cs.cornell.edu/courses/cs5430/2013sp/paper.smithInfoFlow.pdf) - [ ] Terauchi (2008), ["A Type System for Observational Determinism"](https://conferences.computer.org/sp/pdfs/csf/2008/2008-terauchi-type.pdf) - [ ] Clarkson and Schneider (2010), ["Hyperproperties"](https://www.cs.cornell.edu/fbs/publications/Hyperproperties.pdf) - [ ] Clarkson (2016), ["Hyperproperties"](https://www.cs.cornell.edu/courses/cs5430/2016sp/l/27-hyperproperties/lec.pdf) - [ ] Sheff (2013), ["Secure Information Flow by Self-Composition"](https://www.cs.cornell.edu/courses/cs6113/2013fa/notes/Self_Composition.pdf) - [ ] Clarkson et al. (2014), ["Temporal Logics for Hyperproperties"](https://arxiv.org/abs/1401.4492) - [ ] Basin et al. (2015), ["Automated Symbolic Proofs of Observational Equivalence"](https://infsec.ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/publications/pub2015/ASPObsEq.pdf) - [ ] Karimpour et al. (2016), ["Verifying Observational Determinism"](https://inria.hal.science/hal-01345097v1/document) - [ ] Cheval et al. (2018), “DEEPSEC: Deciding Equivalence Properties in Security Protocols—Theory and Practice" - [ ] Cheval et al. (2018), ["The DEEPSEC Prover"](https://link.springer.com/chapter/10.1007/978-3-319-96142-2_4) - [ ] Cheval et al. (2019), [“Exploiting Symmetries When Proving Equivalence Properties for Security Protocols"](https://chevalvi.gitlabpages.inria.fr/chevalvi/files/CKR-ccs19.pdf) - [ ] Knabenhans (2018), ["Automatic Inference of Hyperproperties"](https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Christian_Knabenhans_BA_report.pdf) - [ ] Patrignani (2018), ["(Hyper)Properties, Robustness, and Property-Preserving Compilers"](https://theory.stanford.edu/~mp/mp/CS350-2018_files/cs350-l3-rc.pdf) - [ ] Coenen (2019), ["Verifying Hyperliveness"](https://link.springer.com/chapter/10.1007/978-3-030-25540-4_7) - [ ] Eilers et al. (2019), ["Modular Product Programs"](https://dl.acm.org/doi/10.1145/3324783) - [ ] Babel et al. (2020), “On the Semantics of Communications When Verifying Equivalence Properties" - [x] Wayne (2020), ["Hypermodeling Hyperproperties"](https://hillelwayne.com/post/hyperproperties/) - [ ] Eilers et al. (2021), ["Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security"](https://pmpub.inf.ethz.ch/publications/EilersMeierMueller21.pdf) - [ ] Beutner and Finkbeiner (2022), ["Software Verification of Hyperproperties Beyond *k*-Safety"](https://vetss.org.uk/wp-content/uploads/sites/165/2024/05/2022_2-M-Casadio.pdf) - [ ] Pick (2022), ["Scaling Automatic Modular Verification"](https://lmpick.github.io/thesis.pdf), especially chapter 5, "Verification of Information Flow Security" - [ ] Gutsfeld et al. (2023), ["Deciding Asynchronous Hyperproperties for Recursive Programs"](https://arxiv.org/abs/2201.12859) - [x] Wayne (2024), ["Hyperproperties"](https://buttondown.com/hillelwayne/archive/hyperproperties/) - [x] Finkbeiner (2025), ["Logics and Algorithms for Hyperproperties"](https://arxiv.org/abs/2501.08063v1) ### Theorem provers and proof assistants - ["Logic and Proof"](https://leanprover-community.github.io/logic_and_proof/) - [ ] Chiplunkar and Pit-Claudel (2023), ["Diagrammatic Notations for Interactive Theorem Proving"](https://infoscience.epfl.ch/entities/publication/efc22dde-07ac-4bff-a71b-715f15cd5e99) - [ ] Christiansen (2023), ["Functional Programming in Lean"](https://leanprover.github.io/functional_programming_in_lean/) - [ ] Klavins (2026), ["Automated Mathematics"](https://faculty.washington.edu/klavins/LeanW26/dist/) - [ ] Murphy et al. (2024), ["Autoformalizing Euclidean Geometry"](https://arxiv.org/abs/2405.17216) - [ ] Pit-Claudel (2020), ["Untangling Mechanized Proofs"](https://dl.acm.org/doi/10.1145/3426425.3426940) - [ ] Ringer (2021), ["Proof Repair"](https://homes.cs.washington.edu/~djg/theses/ringer_dissertation.pdf) ## Logic(s) - ["Linear Logic"](https://plato.stanford.edu/entries/logic-linear/), *Stanford Encyclopedia of Philosophy* - [ ] Basin and Constable (1991), ["Metalogical Frameworks"](https://ecommons.cornell.edu/server/api/core/bitstreams/a27793f9-009b-4251-bd1f-674d7d4de215/content) - [ ] Basin et al. (1996), "A Topography of Labelled Modal Logics", in *Frontiers of Combining Systems: First International Workshop, Munich, March 1996* - [ ] Basin et al. (1997), ["Labelled Propositional Modal Logics: Theory and Practice"](https://ieeexplore.ieee.org/abstract/document/8344126) - [ ] Basin et al. (1998), ["Natural Deduction for Non-Classical Logics"](https://link.springer.com/article/10.1023/A:1005003904639) - [ ] Basin et al. (2000), ["Rewriting Logic as as Metalogical Framework"](https://link.springer.com/chapter/10.1007/3-540-44450-5_4) - [ ] Basin and Matthews (2002), ["Logical Frameworks"](https://link.springer.com/chapter/10.1007/978-94-017-0464-9_2), in Gabbay and Guenthner (eds.), *Handbook of Philosophical Logic* - [ ] Jung et al. (2018), ["Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic"](https://people.mpi-sws.org/~dreyer/papers/iris-ground-up/paper.pdf) ## Vulnerabilities and exploits - [ ] Bratus and Shubina (2015), "Exploitation as Code Reuse: On the Need of Formalization" - [ ] Bratus et al. (2011), "Exploit Programming: From Buffer Overflows to 'Weird Machines' and Theory of Computation" - [ ] Dullien (2017), "Weird Machines, Exploitability, and Proven Unexploitability" - [ ] Evtyushkin et al. (2021), "Computing with Time: Microarchitectural Weird Machines" - [ ] Mertens et al. (2019),"Weird Machines as Insecure Compilation" - [ ] Shacham (2007), ["The Geometry of Innocent Flesh on the Bone: Return-into-libc without Function Calls (on the x86)"](https://dl.acm.org/doi/pdf/10.1145/1315245.1315313) - [ ] Vanegue, "Adversarial Logic"