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 proofs are done with: proof assistants, theorem provers, VC generators, decision procedures, logic libraries. Membership: about the tool, not a result obtained with it; renamed tools (Coq/Rocq) count once.
109 references
Deductive verification of active objects with Crowbar
Eduard Kamburjan and others (2023) · Science of Computer Programming · Elsevier BV
VerifMSI: Practical Verification of Hardware and Software Masking Schemes Implementations
Quentin Meunier and others (2023) · 20th International Conference on Security and Cryptography (SECRYPT)
A Coq Library for Mechanised First-Order Logic
Dominik Kirst and others (2022) · The Coq Workshop 2022
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Elizabeth Polgreen and others (2022) · Computer Aided Verification · Springer
Extending a brainiac prover to lambda-free higher-order logic
Petar Vukmirović and others (2022) · International Journal on Software Tools for Technology Transfer
The Isabelle/Isar Reference Manual
Makarius Wenzel (2021)
Gobra: Modular specification and verification of Go programs
Felix A. Wolf and others (2021) · 33rd International Conference on Computer Aided Verification (CAV) · Springer
Boosting SMT solver performance on mixed-bitwise-arithmetic expressions
Dongpeng Xu and others (2021) · ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
Navigating the Universe of Z3 Theory Solvers
Nikolaj Bjørner and others (2020) · Lecture notes in computer science · Springer Science+Business Media
RP-Rewriter: An Optimized Rewriter for Large Terms in ACL2
Mertcan Temel (2020) · Proceedings of the 16th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2020)
The Coq proof assistant reference manual, version 8.10.1
The Coq Development Team (2019) · Oct. 2019: https://coq.inria.fr/
Hammer for Coq: Automation for Dependent Type Theory
Ł. Czajka and others (2018) · Springer Science and Business Media LLC
Smtlink 2.0
Yan Peng and others (2018) · Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2018)
The Proof Complexity of SMT Solvers
Robert Robere and others (2018) · Lecture notes in computer science · Springer Science+Business Media
The VerCors Tool Set: Verification of Parallel and Concurrent Software
Stefan Blom and others (2017) · Integrated Formal Methods · Springer
Kami: A Platform for High-Level Parametric Hardware Specification and Its Modular Verification
Joonwon Choi and others (2017) · Proceedings of the ACM on Programming Languages
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
Burak Ekici and others (2017) · Computer Aided Verification · Springer International Publishing
Meta-extract: Using Existing Facts in Meta-reasoning
Matt Kaufmann and others (2017) · Proceedings of the 14th International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2017)
Accessible Software Verification with Dafny
K. Rustan M. Leino (2017) · IEEE Software · IEEE Computer Society
Isabelles Logics
Lawrence C Paulson (2017) · Available at isabelle
Solving quantified linear arithmetic by counterexample-guided instantiation
Andrew Reynolds and others (2017) · Formal Methods in System Design
Defining (co)datatypes and primitively (co)recursive functions in Isabelle/HOL
J. Biendarra and others (2016)
Decision Procedures
Daniel Kroening and others (2016) · Springer Berlin Heidelberg
Eisbach: A Proof Method Language for Isabelle
Daniel Matichuk and others (2016) · Springer Science and Business Media LLC
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
νZ - An Optimizing SMT Solver
N. Bjørner and others (2015) · Springer Berlin Heidelberg
The Lean Theorem Prover (System Description)
Leonardo de Moura and others (2015) · Lecture notes in computer science · Springer Science+Business Media
νZ - Maximal Satisfaction with Z3
Nikolaj Bjørner and others (2014) · EPiC series in computing
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
30 years of research and development around Coq
Gérard Huet and others (2014) · ACM SIGPLAN Notices · Association for Computing Machinery
The Isabelle/Isar Reference Manual.
Makarius Wenzel (2014)
Why3 — Where Programs Meet Provers
J.-C. Filliâtre and others (2013) · Springer Berlin Heidelberg
dReal: An SMT Solver for Nonlinear Theories over the Reals
Sicun Gao and others (2013) · Lecture notes in computer science · Springer Science+Business Media
Isabelles Logics: FOL and ZF
Lawrence C Paulson (2013) · Available at http://isabelle
Coquet: A Coq Library for Verifying Hardware
Thomas Braibant (2011) · Lecture notes in computer science · Springer Science+Business Media
An introduction to programming and proving with dependent types in coq
Adam Chlipala (2010) · J. Formalized Reasoning
A Quick Tour of the VeriFast Program Verifier
Bart Jacobs and others (2010) · Lecture notes in computer science · Springer Science+Business Media
Dafny: An Automatic Program Verifier for Functional Correctness
K. R. M. Leino (2010) · Springer Berlin Heidelberg
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays
Robert Brummayer and others (2009) · Springer Berlin Heidelberg
Proof assistants: History, ideas and future
Herman Geuvers (2009) · Sādhanā
A Declarative Language for the Coq Proof Assistant
P. Corbineau (2008) · Springer Berlin Heidelberg
Z3: An Efficient SMT Solver
Leonardo de Moura and others (2008) · Lecture notes in computer science · Springer Science+Business Media
A Brief Overview of PVS
Sam Owre and others (2008) · Lecture notes in computer science · Springer Science+Business Media
The Isabelle Framework
M. Wenzel and others (2008) · Springer Berlin Heidelberg
Web Interfaces for Proof Assistants
C. Kaliszyk (2007) · Elsevier BV
KeY-C: A Tool for Verification of C Programs
Oleg Mürk and others (2007) · Springer Berlin Heidelberg
Isabelle/Isar - a generic framework for human-readable proof documents
M. Wenzel (2007) · Studies in Logic, Grammar and Rhetoric
Boogie: A Modular Reusable Verifier for Object-Oriented Programs
Mike Barnett and others (2006) · Lecture notes in computer science · Springer Science+Business Media
A document-oriented Coq plugin for TeXmacs
H. Geuvers and others (2006) · Proceedings of the MathUI workshop at MKM 2006, Wokingham
Verification condition generation via theorem proving
John Matthews and others (2006) · 13th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) · Springer
Verification of Sequential Imperative Programs in Isabelle/HOL
Norbert Schirmer (2006)
Integration of a Software Model Checker into Isabelle
M. Daum and others (2005) · Springer Berlin Heidelberg
Simplify: a theorem prover for program checking
David Detlefs and others (2005) · Journal of the ACM · Association for Computing Machinery
A HOL Theory of Euclidean Space
John Harrison (2005) · Lecture notes in computer science · Springer Science+Business Media
A Mechanically Verified, Sound and Complete Theorem Prover for First Order Logic
Tom Ridge and others (2005) · Theorem Proving in Higher Order Logics · Springer
A Verification Environment for Sequential Imperative Programs in Isabelle/HOL
Norbert Schirmer (2005) · Springer Berlin Heidelberg
Taclets: A New Paradigm for Constructing Interactive Theorem Provers
Bernhard Beckert and others (2004) · RACSAM
Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions
Yves Bertot and others (2004) · Springer Berlin Heidelberg
C-CoRN, the Constructive Coq Repository at Nijmegen
Luı́s Cruz-Filipe and others (2004) · Lecture notes in computer science · Springer Science+Business Media
Taclets and the KeY prover
Martin Giese (2004) · Electronic Notes in Theoretical Computer Science
A New Extraction for Coq
Pierre Letouzey (2003) · Lecture notes in computer science · Springer Science+Business Media
Manip: A PVS Prover Strategy Package for Common Manipulations
B. L. Di Vito (2002) · NASA Langley Research Center, Hampton, VA, 2002. availanle at http://shemesh.larc.nasa.gov/fm/ftp/larc/PVSlibrary/pvslib.html
Isabelle/HOL: A Proof Assistant for Higher-Order Logic
T. Nipkow and others (2002) · Springer Berlin Heidelberg
Isabelle/Isar—a versatile environment for human-readable formal proof documents
Markus Wenzel (2002)
Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS
Andrew A. Adams and others (2001) · Lecture notes in computer science · Springer Science+Business Media
From LCF to HOL: A Short History
Mike Gordon (2000) · The MIT Press
Inductive Datatypes in HOL — Lessons Learned in Formal-Logic Engineering
Stefan Berghofer and others (1999) · Springer Berlin Heidelberg
PVS Language Reference
S. Owre and others (1999) · Computer Science Laboratory, SRI International, Menlo Park, CA, September
PVS System Guide
S. Owre and others (1999) · Computer Science Laboratory, SRI International, Menlo Park, CA, September
A HOL Conversion for Translating Linear Time Temporal Logic to ω-Automata
K. Schneider and others (1999) · Springer Berlin Heidelberg
PVS Prover Guide
N. Shankar and others (1999) · Computer Science Laboratory, SRI International, Menlo Park, CA, September
Using reflection to build efficient and certified decision procedures
Samuel Boutin (1997) · Lecture notes in computer science · Springer Science+Business Media
Proof Planning for Automating Hardware Verification
Francisco Javier Cantu-Ortiz (1997)
A bitvectors library for PVS
R. W. Butler and others (1996) · Technical Report TM-110274
A mizar mode for HOL
John Harrison (1996) · Lecture notes in computer science · Springer Science+Business Media
ACL2: an industrial strength version of Nqthm
Matt Kaufmann and others (1996)
The coq proof assistant reference manual version 5.10
C. Cornes and others (1995) · Tech. Rep.
A tutorial introduction to PVS
J. Crow and others (1995) · Presented at WIFT ’95: Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, Florida, April 1995. Available, with specification files, at http://www.csl.sri.com/wift-tutorial.html
ACL2: A Computational Logic for Applicative Common Lisp, The User’s Manual (Version 1.8)
M. Kaufmann and others (1995) · ftp:// ftp.cli.com/pub/acl2/v1-8/acl2-sources/doc/ HTML/acl2-doc.html
Formal verification for fault-tolerant architectures: prolegomena to the design of PVS
Sam Owre and others (1995) · Institute of Electrical and Electronics Engineers (IEEE)
A tutorial on using PVS for hardware verification
Sam Owre and others (1995) · Lecture notes in computer science · Springer Science+Business Media
Efficiency in a fully-expansive theorem prover
Richard J. Boulton (1994) · Technical Report 337
The HOL Logic and System
M.J.C. Gordon and others (1994) · Elsevier
Modelling bit vectors in HOL: The word library
Wai Wong (1994) · Higher Order Logic Theorem Proving and Its Applications · Springer Berlin Heidelberg
On the comparison of HOL and Boyer-Moore for formal hardware verification
C. M. Angelo and others (1993) · Formal Methods in System Design · Springer Science and Business Media LLC
Introduction to HOL: A Theorem Proving Environment for Higher Order Logic
M. J. C. Gordon and others (1993) · Cambridge University Press
Increasing the versatility of heuristic based theorem provers
Alistair Manning and others (1993) · Lecture notes in computer science · Springer Science+Business Media
Inductive definitions in the system Coq rules and properties
Christine Paulin-Mohring (1993) · Springer-Verlag
Abstract Theories in HOL
Phillip J Windley (1993) · Elsevier
Recording HOL proofs
W. Wong (1993) · University of Cambridge, Computer Laboratory
Analytica — A theorem prover in mathematica
Edmund Clarke and others (1992) · Springer Berlin Heidelberg
PVS: A prototype verification system
Sam Owre and others (1992) · Lecture notes in computer science · Springer Science+Business Media
A Package For Inductive Relation Definitions In HOL
T F Melham (1991) · IEEE
Nuprl as a general logic
Robert L Constable and others (1990) · Logic and computer science · Academic Press
OBJ as a Theorem Prover with Applications to Hardware Verification
Joseph A. Goguen (1989) · Current Trends in Hardware Verification and Automated Theorem Proving · Springer New York
Automating recursive type definitions in higher order logic
Thomas Frederick Melham (1988) · CL Technical Reports
HOL: A Proof Generating System for Higher-Order Logic
Mike Gordon (1987) · University of Cambridge Computer Laboratory
Logic and Computation: Interactive Proof with Cambridge LCF
Lawrence Charles Paulson (1987) · Cambridge University Press
Graph-Based Algorithms for Boolean Function Manipulation
Randal E. Bryant (1986) · IEEE Transactions on Computers · Institute of Electrical and Electronics Engineers
Implementing Mathematics with the NuPRL Proof Development Environment
R. Constable (1986) · Prentice-Hall
Symbolic Manipulation of Boolean Functions Using a Graphical Representation
Randal E. Bryant (1985) · Proceedings of the 22nd ACM/IEEE Design Automation Conference (DAC '85)
HOL: A machine oriented formulation of higher order logic
Mike Gordon (1985) · University of Cambridge Computer Laboratory
LCF LSM
Mike Gordon (1983) · Technical Report 41
LCF_LSM: A system for specifying and verifying hardware
Mike Gordon (1983) · University of Cambridge Computer Laboratory
Representing a logic in the LCF metalanguage
M. J. C. Gordon (1982) · Tools and Notions for Program Construction · Cambridge University Press
How to derive inductions in LCF
R. Milner (1980) · The University of Edinburgh
Edinburgh LCF: A Mechanised Logic of Computation
Michael J. C. Gordon and others (1979) · Springer Berlin Heidelberg
Lcf: A way of doing proofs with a machine
Robin Milner (1979) · Lecture notes in computer science · Springer Science+Business Media