This repository was originally intended as a log of my learning of the Coq proof assistant. My interests have since grown enormously in breadth and so the document has surpassed its original scope. At this moment, I'd like this place to collect and categorise interesting and useful resources on the theory and applications of various methods of formal verification. This includes topics such as theorem proving, higher-order logic, lambda calculus, type theory, model checking, automated reasoning and so on.
During my adventures in the software verification land, I too often grieved that there was no single book or website that would concisely and eloquently describe some of the methods of the field, the software packages it employed, the jargon or connections to other fields of research. To the best of my knowledge, there is still no such book, survey article, podcast or any other resource. My vision is to fill this gap and provide a sort of signpost or handbook for readers who are new to this area and are eager to learn all of it.
I do not yet claim completeness, correctness, consistency or usefulness of any of information contained herein.
- Useful resources on Coq
- Libraries and plug-ins for Coq
- Applications of Coq
- Related languages, tools and stuff
- Type theory
- Copyright
Useful resources on Coq
- Official Coq documentation
- The official documentation is OK, quite comprehensive. The description of tactics is very good, there are few undocumented points.
- Reference Manual
- Tutorial
- A simple and straightforward introduction to basics of proofs using Coq
- Official wiki on GitHub
- The coq-club mailing list
- B. C. Pierce et al.: Software Foundations – probably the best introduction into Coq and theorem proving available
- A. Chlipala: Certified Programming with Dependent Types – an awesome book to read after Software Foundations; a bit more advanced, slightly different topics; puts forth the idea of using automation whenever possible
- I. Sergey: Programs and Proofs: Mechanizing Mathematics with Dependent Types (draft)
- /r/coq
- Coq in a Hurry
- Introduction to the Coq proof-assistant for practical software
verification course notes
- Another tutorial, slightly more interesting; possibly outdated
- Coq'Art – the first ever
book on Coq and CoC
- See also Pierre Castéran's page for A Tutorial on [Co-]Inductive Types in Coq and A Gentle Introduction to Type Classes and Relations in Coq
- the nLab wiki
- its page on Coq, for instance
Coq-related blogs
- Poleiro
- Gagallium – blog of the Gallium research team at Inria
- Guillaume Claret's Coq blog
- Coq en Stock
- Homotopy Type Theory blog
- Modules for Modalities – an article on Coq's module system and universe polymorphism
- The Type Theory Podcast
Libraries and plug-ins for Coq
- Ssreflect and MathComp
- CoLoR – "a Coq Library on rewriting and termination"
- coq-ext-lib – "a collection of theories and plugins that may be useful in other Coq developments"
- std++ – an extended standard library
- Equations – dependent pattern matching
- Mtac – "a monad for typed tactic programming in Coq"
- coq-dpdgraph – plug-in for exploring dependencies between Coq objects
- wilcoxjay/tactics – some useful tactics by James Wilcox
- "A Formal Library for Elliptic Curves in the Coq Proof Assistant" (GitHub)
- Coquelicot – library for real analysis
- C. Lelay (2015): "How to express convergence for analysis in Coq"
- Coq.io and others by Guillaume Claret (GitHub)
- coq-haskell
- Applied: coq-pipes
- CFML: Characteristic Formulae for ML
– verification of correctness and amortized complexity of OCaml programs
- A series of blog posts on the Gagallium blog on verifying complexity
- Verified Software Toolchain (VST)
- tons of articles around this
- A. W. Appel: "Verified Software Toolchain" (2011)
- A. W. Appel: "Verification of a Cryptographic Primitive: SHA-256" (2016)
- "Category Theory in Coq 8.5" (Bitbucket; Coq Workshop 2014)
- CH2O – formalization of ISO C11 by Rober Krebbers (GitHub)
Applications of Coq
- CompCert – verified optimising compiler of
a substantial subset of C99
- X. Leroy et al.: "CompCert – A Formally Verified Optimizing Compiler" (2016)
- Verasco – verified static analyser
- DopCert – framework for formally verifying database query optimizations; uses HoTT
- S. Chu, K. Weitz, A. Cheung, D. Suciu: "HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics" (2016)
- JSCert: Certified JavaScript
- Cosa – Coq-verified Shape Analysis
- "A Machine-Checked Proof of the Odd Order Theorem"
- "A Reflexive Formalization of a SAT Solver in Coq" (2008)
- "Towards an effective formally certified constraint solver" (2014; slides)
Papers and articles using Coq
- Heq: a Coq library for Heterogeneous Equality
- "Inductive-inductive definitions"
- "Gradual Certified programming in Coq"
- "An intro to (co)algebra and (co)induction"
- "Canonical Structures for the Working Coq User"
- "Foundational Property-Based Testing" – QuickChick, a port of QuickCheck to Coq
- J. Gross: "Coq Bug Minimizer" (CoqPL 2015; GitHub)
- C. Doczkal, J.-O. Kaiser, G. Smolka: "A Constructive Theory of Regular Languages in Coq"
- F. Chyzak, A. Mahboubi, T. Sibut-Pinote, E. Tassi: "A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)"
- HAL Loria Archive, (Department 2: Formal Methods](https://hal.inria.fr/LORIA-FM/index/index)
Related languages, tools and stuff
For tools, see also page on the Coq website.
- DeepSpec: The Science of Deep Specification – an NSF-funded initiative aiming to unify existing tools at the specification level and develop new ways to write "good" specifications
- Homotopy Type Theory – the book and the library
- Coq for Homotopy Type Theory – a dedicated research project
- UniMath (Univalent Foundations)
- Queensland Functional Programming Lab
Related ACM Special Interest Groups: SIGPLAN, SIGLOG and SIGACT.
Journals and book series
(† denotes open-access journals)
- Logical Methods in Computer Science †
- Electronic Proceedings in Theoretical Computer Science (EPTCS) †
- LIPIcs: Leibniz International Proceedings in Informatics †
- International Journal of Foundations of Computer Science
- Information and Computation
- Journal of Automated Reasoning
- Studies in Logic, Grammar and Rhetoric †
- Springer's Lecture Notes in Computer Science series
Meta
- ACM Journals/Transactions
- Elsevier journals on computer science
- Springer journals on CS
- Cambridge Journals on CS
Conferences and workshops
See the standalone file.
Proof assistants, provers and languages
- Lean – a new theorem prover developed by Microsoft and CMU with automation support; based on CIC, supports HoTT as well
- Matita – based on (a variant of) CoC
- Agda – a (relatively) new, hip dependently-typed functional language and interactive theorem prover
- Idris – another new and hip "general purpose" language with dependent types, support for theorem proving and tactics; kind of like Coq-flavoured Haskell
- Dedukti – proof checker based on the λΠ-calculus; tools for translation from other proof assistants available
- the PRL Project a.k.a. Nuprl
- MetaPRL
- JonPRL (GitHub) – a reimplementation of Nuprl by Jon Sterling, Danny Gratzer and Vincent Rahli
- Red JonPRL – yet another reincarnation by Jon Sterling
- MetaPRL
- miniprl – a minimal implementation of PRL in Standard ML
- cha – an implementation in Haskell
- Isabelle – great Archive of Formal Proofs;
small trusted meta-logical core, usually used along with HOL
- Haskabelle
- Isar
- Isabelle/HOLCF – paper, tutorial
- Archive of Formal Proofs – an extensive collection of proof libraries for Isabelle
- HOL by Michael Gordon et al. – the original system for interactive theorem proving in higher-order logic
- MINLOG – interactive proof assistant based on first-order natural deduction calculus
- ProofPower – based on higher-order logic
- Mizar
- ACL2 (A Computational Logic for Applicative Common Lisp) – logic for modelling systems and a complementary prover; based on first-order logic
- Milawa – theorem prover for ACL2-like logic
- ATS (Applied Type System) – dependently typed functional languge
- E theorem prover for first-order logic
- LEGO proof assistant
- F7 – extension of F#'s type system with refinement types, dependent types and π-calculus-style concurrency
- F* – "a new higher order, effectful programming language designed with program verification in mind"
- Eff – functional language with first-class effects and native handling of all kinds of computational effects without touching monads
- Twelf
- Celf
- Abella
- Beluga
- Delphin
- C. Schürmann, R. Fontana, Y. Liao: "Delphin: Functional Programming with Deductive Systems"
- Andromeda – type theory with equality reflection
- Andrej Bauer's Leeds workshop slides and some interesting discussion in the comments below
- Prover9 and Mace4 – and automated theorem prover for FOL and searcher for counterexamples, respectively
- leanCOP – tiny automated theorem prover for classical first-order logic implemented in Prolog
- PVS
- Guru
- A. Stump, et al.: "Verified Programming in Guru"
- MMT language and system
See also: Every proof assistant series of lectures.
- Coq
- Coq is an interactive theorem prover and proof assistant based on an intensional intuitionistic type theory -- the Calculus of Inductive Constructions (CIC). It is a dependently-typed λ-calculus and (by the Curry-Howard isomorphism) an intuitionistic higher-order logic. It is written in OCaml.
Model checkers
- SPIN
- DIVINE – parallel, distributed-memory explicit-state LTL checker
- UPPAAL
- TLA+
- NuSMV – symbolic model checker
- Ultimate Automizer – model checker based on an automata approach
- LTSmin – language-agnostic
- PRISM – probabilistic model checker
- MMC – explicit-state model checker for π-calculus
- CBMC – bounded model checking
- ESBMC – context-bounded model checking
- Nidhugg
SAT & SMT solvers
- MiniSat
- PicoSAT
- Z3
- CVC4
- Alt-Ergo (academic page)
- Yices (non-free licence)
- MathSAT 5
- Boolector
- Lingeling, Plingeling and Treengeling
- CryptoMiniSat 2
- CaDiCaL
- SONOLAR – Solver for Non-Linear Arithmetic
- ABC – "A System for Sequential Synthesis and Verification"
- Vampire
- zChaff
- funsat – "a modern DPLL-style SAT solver" written in Haskell
- versat
- D. Oe, A. Stump, C. Oliver, K. Clancy: "versat: A Verified Modern SAT Solver" (2011)
- "Simple SMT solver for use in an optimizing compiler"
- SAT Competitions
- Configurable SAT Solver Challenge (CSSC) 2014
- Model Checking Contest (MCC)
Other tools
- Why3 – platform for deductive reasoning on programs with support for many external provers
- Alloy – "a language and tool for relational models"
- Boogie – intermediate verification language
- Q Program Verifier
– collection of tools for a source–IR–IVL translation and subsequent verification
- SMACK – bounded verification via LLVM to Boogie translation
- Dafny – "a language and program verifier for functional correctness"
- Vienna Verification Toolkit
- CSeq
- IKOS – "library designed to facilitate the development of sound static analyzers based on Abstract Interpretation"
- Crab – "language agnostic engine to perform static analysis based on abstract interpretation"
- Seahorn – "fully automated verification framework for LLVM-based languages"
- rise4fun – a collection of numerous tools, i.a. for program and algorithm analysis and verification, by Microsoft Research, CMU and others that you can try right on the web page
- Profound – "an experiment in
subformula linking as an interaction method"
- K. Chaudhuri: "Subformula Linking as an Interaction Method" (2013)
- S²E – "A Platform for In-Vivo Analysis of Software Systems"
- KLEE – symbolic execution VM
- CPAchecker
- Ultimate
- K Framework
- Lem
Formal methods in practice
- Muen Separation Kernel – first open-source kernel verified for absence of runtime errors (Reddit discussion)
- CertiKOS – "advanced development of certified OS kernels"
- Galois, Inc.
- Software Systems Research Group (SSRG) at NICTA – tons of exciting projects
Learning resources
Courses, textbooks, papers, theses, competitions, influential figures in the field.
-
The QED Manifesto, some more details here
-
VerifyThis – a competition and collection of problems in formal verification of algorithms and software
-
Competition on Software Verification (SV-COMP)
-
Oregon Programming Languages Summer School – video recordings of awesome lectures on type theory, provers, logic, etc.; earlier editions only have lecture notes and slides published
2016, 2015, 2014, 2013, 2012, 2011, 2010, 2009, 2008, 2007, 2006, 2005
Type theory
Danny Gratzer's learn-tt is a fantastic resource for those interested in type and category theory. He presents all the terrific tools, textbooks, and papers that deal with both of these in a sensible and logical way, which is a quality that my repository will never have.
I'll only list here resources which he doesn't mention and which I personally find interesting.
Check out the TYPES mailing list as well.
Dependent types
- C. McBride: Epigram: Practical Programming with Dependent Types (2010)
- A. Bove, P. Dybjer: Dependent Types at Work – introduction to programming with dependent types in Agda
Observational Type Theory
- T. Altenkirch, C. McBride: "Towards Observational Type Theory" (2006)
- F. Mazzoli: "Bertus: Implementing Observational Equality" (2013)
Univalent Foundations and Homotopy Type Theory
- P. Aczel: "On Voevodsky's Univalence Axiom" (2011; slides)
Cubical Type Theory
- M. Bezen, T. Coquand, S. Huber: "A model of type theory in cubical sets" (2014)
- D. Licata: "A Cubical Type Theory" (2014; slides)
- A. Kaposi, T. Altenkirch: "A syntax for cubical type theory" (2014; slides)
- T. Coquand: "A Cubical Type Theory" (2015; slides)
- T. Coquand: "A cubical type theory" (2015; slides)
- C. Cohen, T. Coquand, S. Huber, A. Mörtberg: "Cubical Type Theory: a constructive interpretation of the univalence axiom" (2016)
- mortberg/cubicaltt – a Haskell implementation of the type theory presented in this paper
Copyright
Written in 2015–2020 by Matěj Grabovský
This work is licensed under a Creative Commons Attribution 4.0 International License.