This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
What one proves with
A subject the papers are about. The loosest grouping, and the one to reach for last.
The tools the proofs are actually done with: proof assistants, theorem provers, verification condition generators, decision procedures, and the libraries formalising logic itself. Every result in the other verification sets rests on one of these, and a tool built for one language belongs here as much as a general one. Membership requires the work to be about the tool rather than about a result obtained with it, and follows the tool through its renamings -- Coq and Rocq are one member of this set, not two.
17 references
Completeness of Iris-Based Program Logics
Johannes Hostert and others (2026) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery (ACM)
Deductive verification of active objects with Crowbar
Eduard Kamburjan and others (2023) · Science of Computer Programming · Elsevier BV
Undecidability of dyadic first-order logic in Coq
Johannes Hostert and others (2022) · 13th International Conference on Interactive Theorem Proving (ITP 2022) · Schloss Dagstuhl – Leibniz-Zentrum für Informatik
A Coq Library for Mechanised First-Order Logic
Dominik Kirst and others (2022) · The Coq Workshop 2022
Extending a brainiac prover to lambda-free higher-order logic
Petar Vukmirović and others (2022) · International Journal on Software Tools for Technology Transfer
Gobra: Modular specification and verification of Go programs
Felix A. Wolf and others (2021) · 33rd International Conference on Computer Aided Verification (CAV) · Springer
The VerCors Tool Set: Verification of Parallel and Concurrent Software
Stefan Blom and others (2017) · Integrated Formal Methods · Springer
Solving quantified linear arithmetic by counterexample-guided instantiation
Andrew Reynolds and others (2017) · Formal Methods in System Design
Viper: A verification infrastructure for permission-based reasoning
Peter Müller and others (2016) · Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings 17 · Springer
The VerCors tool for verification of concurrent programs
Stefan Blom and others (2014) · International Symposium on Formal Methods · Springer
OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse
David R. Cok (2014) · Formal Integrated Development Environment 2014 (F-IDE 2014) · Open Publishing Association
The 1st Verified Software Competition: Experience Report
Vladimir Klebanov and others (2011) · FM 2011: Formal Methods · Springer
Proof assistants: History, ideas and future
Herman Geuvers (2009) · Sādhanā
Verification condition generation via theorem proving
John Matthews and others (2006) · 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) · Springer
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic
Tom Ridge and others (2005) · Theorem Proving in Higher Order Logics · Springer
Taclets: A New Paradigm for Constructing Interactive Theorem Provers
Bernhard Beckert and others (2004) · RACSAM
Taclets and the KeY prover
Martin Giese (2004) · Electronic Notes in Theoretical Computer Science