Fetching the paper…
Reading the bibliography…
Mechanical reasoning is a key area of research that lies at the crossroads of mathematical logic and artificial intelligence.
On the rules of supposition in formal logic
S. Jaskowski · 1934
Earlier work this paper cites.
A machine program for theorem-proving
M. Davis, G. Logemann, and D. Loveland · 1962
Earlier work this paper cites.
Cooperating sequential processes
E. W. Dijkstra · 1968
Earlier work this paper cites.
The complexity of theorem-proving procedures
S. A. Cook · 1971
Earlier work this paper cites.
The prehistory and early history of automated deduction
M. Davis · 1983
Earlier work this paper cites.
Geo prover- A geometry theorem prover developed at UT
S. J. Chou · 1986
Earlier work this paper cites.
Implementing Mathematics with the Nuprl proof development system
R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith · 1986
Earlier work this paper cites.
Logic and Computation: Interactive Proof with Cambridge LCF
L. C. Paulson · 1987
Earlier work this paper cites.
The calculus of constructions
T. Coquand and G. Huet · 1988
Earlier work this paper cites.
Lambda-Prolog: An extended logic programming language
A. P. Felty, E. L. Gunter, J. Hannan, D. Miller, G. Nadathur, and A. Scedrov · 1988
Earlier work this paper cites.
Computer theorem proving and artificial intelligence
H. Wang · 1990
Earlier work this paper cites.
The Boyer-Moore prover and Nuprl: An experimental comparison, logical frameworks, 1991
D. Basin and M. Kaufmann · 1991
Earlier work this paper cites.
Verifying a logic synthesis tool in Nuprl: A case study in software verification
M. Aagaard and M. Leeser · 1992
Earlier work this paper cites.
Using Nuprl for the verification and synthesis of hardware
M. Lesser · 1992
Earlier work this paper cites.
SETHEO: A high-performance theorem prover
R. Letz, J. Schuman, S. Bayerl, and W. Bibel · 1992
Earlier work this paper cites.
Report of the inquiry into the london ambulance service, 1993
D. Page · 1993
Earlier work this paper cites.
Verification of real-time systems using PVS
N. Shankar · 1993
Earlier work this paper cites.
The QED manifesto
R. Boyer · 1994
Earlier work this paper cites.
Otter 3.0 reference manual and guide
W. W. McCune · 1994
Earlier work this paper cites.
A tutorial on using PVS for hardware verification
S. Owre, J. M. Rushby, N. Shankar, and M. K. Srivas · 1994
Earlier work this paper cites.
Isabelle: A generic theorem prover
L. C. Paulson · 1994
Earlier work this paper cites.
Experiments with ZF set theory in HOL and Isabelle
S. Agerholm and M. Gordon · 1995
Earlier work this paper cites.
System safety and computers
N. G. Levenson · 1995
Earlier work this paper cites.
The automation of proof: A historical and sociological exploration
D. Mackenzie · 1995
Earlier work this paper cites.
Structural cut elimination
F. Pfenning · 1995
Earlier work this paper cites.
Assertional specification and verification using PVS of the steam boiler control system
J. Vitt and J. Hooman · 1995
Earlier work this paper cites.
A comparison of HOL and ALF formalizations of a categorical coherence theorem
S. Agerholm, I. Beylin, and P. Dybjer · 1996
Earlier work this paper cites.
Evolutionary Algorithms in Theory and Practice
T. Back · 1996
Earlier work this paper cites.
A Mizar mode for HOL
J. Harrison · 1996
Earlier work this paper cites.
Semantic foundations for embedding HOL in Nuprl
D. J. Howe · 1996
Earlier work this paper cites.
Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods
M. K. Srivas and S. P. Miller · 1996
Earlier work this paper cites.
The impact of the lambda calculus in logic and computer science
H. Barendregt · 1997
Earlier work this paper cites.
A hybrid approach to verifying liveness in a symmetric multiprocessor
J. Camilleri · 1997
Earlier work this paper cites.
Waldmeister: High performance equational deduction
T. Hillenbrand, A. Buch, R. Vogt, and B. Lochner · 1997
Earlier work this paper cites.
A comparison of the Coq and HOL proof systems for specifying hardware
L. Jakubiec, S. Coupet-Grimal, and P. Curzon · 1997
Earlier work this paper cites.
An industrial strength theorem prover for a logic based on Common Lisp
M. Kaufmann and J. S. Moore · 1997
Earlier work this paper cites.
A comparison of PVS and Isabelle/HOL
D. Griffioen and M. Huisman · 1998
Earlier work this paper cites.
Specification of an integrated circuit card protocol application using the B method and linear temporal logic
J. Julliand, B. Legeard, T. Machicoane, B. Parreaux, and B. Tatibouèt · 1998
Earlier work this paper cites.
Formalising C in HOL
M. Norrish · 1998
Earlier work this paper cites.
A mechanical analysis of program verification strategies
J. S. Moore · 1999
Earlier work this paper cites.
System description: Twelf-a meta-logical framework for deductive systems
F. Pfenning and C. Schürmann · 1999
Earlier work this paper cites.
The Nuprl open logical environment
S. Allen, R. Constable, R. Eaton, C. Kreitz, and L. Lorigo · 2000
Earlier work this paper cites.
A tactic language for the system Coq
D. Delahaye · 2000
Earlier work this paper cites.
Failures of healthcare systems
J. Mackie and I. Sommerville · 2000
Earlier work this paper cites.
Proving theorems about Java-Like byte code
J. S. Moore · 2000
Earlier work this paper cites.
Foundational proof-carrying code
A. W. Appel · 2001
Earlier work this paper cites.
Proof-assistants using dependent type systems
H. Barendregt and H. Geuvers · 2001
Earlier work this paper cites.
Proving hybrid protocols correct
M. Bickford, C. Kreitz, R. van Renesse, and X. Liu · 2001
Earlier work this paper cites.
Verified lightweight bytecode verification
G. Klein and T. Nipkow · 2001
Earlier work this paper cites.
The HOL/NuPRL proof translator
P. Naumov, M.-O. Stehr, and J. Meseguer · 2001
Earlier work this paper cites.
Vampire 1.1 (system description)
A. Riazanov and A. Voronkov · 2001
Earlier work this paper cites.
Evaluating general purpose automated theorem proving systems
G. Sutcliffe and C. Suttner · 2001
Earlier work this paper cites.
Hoare logic for Java in Isabelle/HOL
D. von Oheimb · 2001
Earlier work this paper cites.
Mizar Light for HOL Light
F. Wiedijk · 2001
Earlier work this paper cites.
Enabling hardware verification through design changes
A. T. Abdel-Hamid, S. Tahar, and J. Harrison · 2002
Earlier work this paper cites.
A survey on embedding programming logics in a theorem prover
A. Azurat and W. Prasetya · 2002
Earlier work this paper cites.
Autarkic computations in formal proofs
H. Barendregt and E. Barendsen · 2002
Earlier work this paper cites.
Development of an embedded verifier for Java card byte code using formal methods
L. Casset · 2002
Earlier work this paper cites.
Formal verification of microprocessors at AMD
A. Flatau, M. Kaufmann, D. Reed, D. Russinoff, E. Smith, and R. Sumners · 2002
Earlier work this paper cites.
A constructive algebraic hierarchy in Coq
H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg · 2002
Earlier work this paper cites.
Formal verification of functional properties of an SCR-style software requirements specification using PVS
T. Kim, D. Stringer-Calvert, and S. Cha · 2002
Earlier work this paper cites.
Isabelle/HOL - A proof assistant for higher-order logic
T. Nipkow, L. C. Paulson, and M. Wenzel · 2002
Earlier work this paper cites.
E-A brainiac theorem prover
S. Schulz · 2002
Earlier work this paper cites.
A comparison of Mizar and Isar
W. F. Wenzel, M · 2002
Earlier work this paper cites.
A Nuprl–PVS connection: Integrating libraries of formal mathematics
S. F. Allen, M. Bickford, R. Constable, R. Eaton, and C. Kreitz · 2003
Earlier work this paper cites.
Toward a foundational typed assembly language
K. Crary · 2003
Earlier work this paper cites.
Perfect developer: A tool for object-oriented formal specification and refinement
D. Crocker · 2003
Earlier work this paper cites.
An extensible SAT-solver
N. Eén and N. Sörensson · 2003
Earlier work this paper cites.
New directions in instantiation-based theorem proving
H. Ganzinger and K. Korovin · 2003
Earlier work this paper cites.
Translating Mizar for first order theorem provers
J. Urban · 2003
Earlier work this paper cites.
Safe object-oriented software: The verified design-by-contract paradigm
D. Crocker · 2004
Earlier work this paper cites.
Building reliable, high-performance networks with the Nuprl proof development system
C. Kreitz · 2004
Earlier work this paper cites.
A tool for automated theorem proving in Agda
F. Lindblad and M. Benke · 2004
Earlier work this paper cites.
The B-book: Assigning programs to meanings
J. R. Abrial · 2005
Earlier work this paper cites.
ProofPower–SLRP user guide
R. Arthan · 2005
Earlier work this paper cites.
Using B as a high level programming language in an industrial project: Roissy VAL
F. Badeau and A. Amelot · 2005
Earlier work this paper cites.
A programming logic for distributed systems
M. Bickford and D. Guaspari · 2005
Earlier work this paper cites.
Verifying compilers for financial applications
D. Crocker · 2005
Earlier work this paper cites.
Generating commercial web applications from precise requirements and formal specifications
D. Crocker and J. H. Warren · 2005
Earlier work this paper cites.
Reasoning about functional programs in Nuprl
D. J. Howe · 2005
Earlier work this paper cites.
Mizar: The first 30 years
R. Matuszewski and P. Rudnicki · 2005
Earlier work this paper cites.
Circuits as streams in Coq: Verification of a sequential multiplier
C. Paulin-Mohring · 2005
Earlier work this paper cites.
First-orderized researchcyc : Expressivity and efficiency in a common-sense ontology
D. Ramachandran, P. Reagan, and K. Goolsbery · 2005
Earlier work this paper cites.
Innovations in computational type theory using Nuprl
S. F. Allen, M. Bickford, R. L. Constable, R. Eaton, C. Kreitz, L. Lorigo, and E. Moran · 2006
Earlier work this paper cites.
Splitting on demand in SAT modulo theories
C. Barrett, R. Nieuwenhuis, A. Oliveras, and C. Tinelli · 2006
Earlier work this paper cites.
Research perspectives for logic and deduction
W. Bibel · 2006
Earlier work this paper cites.
Formal verification of a C compiler front-end
S. Blazy, Z. Dargaye, and X. Leroy · 2006
Earlier work this paper cites.
An empirical evaluation of automated theorem provers in software certification
E. Denney, B. Fischer, and J. Schumann · 2006
Earlier work this paper cites.
An embedding of the ACL2 logic in HOL
M. J. C. Gordon, W. A. Hunt, M. Kaufmann, and J. Reynolds · 2006
Earlier work this paper cites.
An integration of HOL and ACL2
M. J. C. Gordon, J. Reynolds, W. A. Hunt, and M. Kaufmann · 2006
Earlier work this paper cites.
OMDoc - An Open Markup Format for Mathematical Documents [version 1.2]
M. Kohlhase · 2006
Earlier work this paper cites.
The three gap theorem (steinhauss conjecture)
M. Mayero · 2006
Earlier work this paper cites.
Importing HOL into Isabelle/HOL
S. Obua and S. Skalberg · 2006
Earlier work this paper cites.
Adding parallelism capabilities to ACL2
D. L. Rager · 2006
Cited alongside, same era.
Tutorial: Automated formal methods with PVS, SAL, and Yices
J. M. Rushby · 2006
Cited alongside, same era.
An executable formalization of the HOL/Nuprl connection in the meta-logical framework Twelf
C. Schurmann and M. Stehr · 2006
Cited alongside, same era.
Lectures on the Curry-Howard Isomorphism
M. H. Sorensen and P. Urzyczyn · 2006
Cited alongside, same era.
The seventeen provers of the world: Foreword by Dana S. Scott
F. Wiedijk · 2006
Cited alongside, same era.
Formal methods: Theory becoming practice
J. R. Abrial · 2007
Cited alongside, same era.
Formal verification of medical device user interfaces using PVS
P. Masci, Y. Zhang, P. Jones, P. Curzon, and H. Thimbleby · 2014
Later among the works it cites.
SAT-enhanced Mizar proof checking
A. Naumowicz · 2014
Later among the works it cites.
Verification for ASP denotational semantics: A case study using the PVS theorem prover
F. Aguado, P. Ascariz, P. Cabalar, G. Perez, and C. Vidal · 2015
Later among the works it cites.
Mining the archive of formal proofs
J. C. Blanchette, M. P. L. Haslbeck, D. Matichuk, and T. Nipkow · 2015
Later among the works it cites.
Models for Metamath
M. Carneiro · 2015
Later among the works it cites.
Pi-Ware: Hardware description and verification in Agda
J. P. P. Flor, W. Swierstra, and Y. Sijsling · 2015
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…
Lessons from applying the systematic literature review process within the software engineering domain
P. Brereton, B. A. Kitchenham, D. Budgen, M. Turner, and M. Khalil · 2007
Cited alongside, same era.
A declarative language for the Coq proof assistant
P. Corbineau · 2007
Cited alongside, same era.
Verification of C programs using automated reasoning
D. Crocker and J. Carlton · 2007
Cited alongside, same era.
Floating-point verification
J. Harrison · 2007
Cited alongside, same era.
A short survey of automated reasoning
J. Harrison · 2007
Cited alongside, same era.
Formal methods in safety-critical railway systems
T. Lecomte, T. Servat, and G. Pouzancre · 2007
Cited alongside, same era.
Logic for Computer Science: Foundations of automatic theorem proving
J. H. Gallier · 2015
Later among the works it cites.
Formal verification methods
O. Hasan and S. Tahar · 2015
Later among the works it cites.
Hol(y)hammer: Online ATP service for HOL Light
C. Kaliszyk and J. Urban · 2015
Later among the works it cites.
Hol(y)hammer: Online ATP service for HOL Light
C. Kaliszyk and J. Urban · 2015
Later among the works it cites.
MizAR 40 for Mizar 40
C. Kaliszyk and J. Urban · 2015
Later among the works it cites.
Formalising type-logical grammars in Agda
W. Kokke · 2015
Later among the works it cites.
Modeling and verification of component connectors in Coq
Y. Li and M. Sun · 2015
Later among the works it cites.
A survey of interactive theorem proving
F. Marić · 2015
Later among the works it cites.
Using PVS to support the analysis of distributed cognition systems
P. Masci, P. Curzon, D. Furniss, and A. Blandford · 2015
Later among the works it cites.
Extending ACL2 with SMT solvers
Y. Peng and M. R. Greenstreet · 2015
Later among the works it cites.
Coq as a metatheory for Nuprl with bar induction
V. Rahli and M. Bickford · 2015
Later among the works it cites.
Playing with AVATAR
G. Reger, M. Suda, and A. Voronkov · 2015
Later among the works it cites.
Automated verification of role-based access control policies constraints using Prover9
K. E. Sabri · 2015
Later among the works it cites.
Experiments with state-of-the-art automated provers on problems in tarskian geometry
J. Urban and R. Veroff · 2015
Later among the works it cites.
An Isabelle/HOL formalisation of Green’s theorem
M. Abdulaziz and L. C. Paulson · 2016
Later among the works it cites.
Proving non-deterministic computations in Agda
S. Antoy, M. Hanus, and S. Libby · 2016
Later among the works it cites.
Certified context-free parsing: A formalisation of Valiant’s algorithm in Agda
J. P. Bernardy and P. Jansson · 2016
Later among the works it cites.
Hammering towards QED
J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban · 2016
Later among the works it cites.
Formalization of real analysis: A survey of proof assistants and libraries
S. Boldo, C. Lelay, and G. Melquiond · 2016
Later among the works it cites.
Formalization of the prime number theorem and Dirichlet’s theorem
M. Carneiro · 2016
Later among the works it cites.
Conversion of HOL Light proofs into Metamath
M. M. Carneiro · 2016
Later among the works it cites.
The scope and limits of simulation in automated reasoning
E. Davis and G. Marcus · 2016
Later among the works it cites.
Two-way automata in Coq
C. Doczkal and G. Smolka · 2016
Later among the works it cites.
Using vampire in soundness proofs of type systems
S. Grewe, S. Erdweg, and M. Mezini · 2016
Later among the works it cites.
Extending E prover with similarity based clause selection strategies
J. Jakubuv and J. Urban · 2016
Later among the works it cites.
Towards a Mizar environment for Isabelle: Foundations and language
C. Kaliszyk, K. Pak, and J. Urban · 2016
Later among the works it cites.
An introduction to mechanized reasoning
M. Kerber, C. Lange, and C. Rowat · 2016
Later among the works it cites.
Formalization of polynomially bounded and negligible functions using the computer-aided proof-checking system Mizar
H. Okazaki and Y. Futa · 2016
Later among the works it cites.
Formal specification of Multi-Window user interface in PVS
K. Singh and B. Auernheimer · 2016
Later among the works it cites.
RedPRL–The people’s refinement logic, available at: http://www.redprl.org/, 2016
J. Sterling, D. Gratzer, V. Rahli, D. Morrison, E. Akentyev, and A. Tosun · 2016
Later among the works it cites.
The CADE ATP system competition - CASC
G. Sutcliffe · 2016
Later among the works it cites.
Automatically proving mathematical theorems with evolutionary algorithms and proof assistants
L. A. Yang, J. P. Liu, C. H. Chen, and Y. ping Chen · 2016
Later among the works it cites.
Formalization of Pell’s equations in the Mizar system
M. Acewicz and K. Pak · 2017
Later among the works it cites.
A formal proof of the expressiveness of deep learning
A. Bentkamp, J. C. Blanchette, and D. Klakow · 2017
Later among the works it cites.
A framework for asynchronous circuit modeling and verification in ACL2
C. K. Chau, W. A. Hunt, M. Roncken, and I. E. Sutherland · 2017
Later among the works it cites.
A formal proof in Coq of LaSalles’s invariance principle
C. Cohen and D. Rouhling · 2017
Later among the works it cites.
Proving divide and conquer complexities in Isabelle/HOL
M. Eberl · 2017
Later among the works it cites.
Smtcoq: A plug-in for integrating SMT solvers into Coq
B. Ekici, A. Mebsout, C. Tinelli, C. Keller, G. Katz, A. Reynolds, and C. W. Barrett · 2017
Later among the works it cites.
Certified password quality - A case study using Coq and Linux pluggable authentication modules
J. F. Ferreira, S. A. Johnson, A. Mendes, and P. J. Brooke · 2017
Later among the works it cites.
Formalizing basic quaternionic analysis
A. Gabrielli and M. Maggesi · 2017
Later among the works it cites.
Tactictoe: Learning to reason with HOL4 tactics
T. Gauthier, C. Kaliszyk, and J. Urban · 2017
Later among the works it cites.
Proof certificates in PVS
F. Gilbert · 2017
Later among the works it cites.
The x86isa books: Features, usage, and future plans
S. Goel · 2017
Later among the works it cites.
Towards an abstraction-refinement framework for reasoning with large theories
J. C. L. Hernandez and K. Korovin · 2017
Later among the works it cites.
Formalizing a fragment of combinatorics on words
S. Holub and R. Veroff · 2017
Later among the works it cites.
Markov chains and markov decision processes in Isabelle/HOL
J. Hölzl · 2017
Later among the works it cites.
Using Coq for formal modeling and verification of timed connectors
W. Hong, M. S. Nawaz, X. Zhang, Y. Li, and M. Sun · 2017
Later among the works it cites.
Proving theorems by using evolutionary search with human involvement
S. Huang and Y. Chen · 2017
Later among the works it cites.
Industrial hardware and software verification with ACL2
W. A. Hunt, M. Kaufmann, J. S. Moore, and A. Slobodova · 2017
Later among the works it cites.
Relating system F and Lambda2: A case study in Coq, Abella and Beluga
J. Kaiser, B. Pientka, and G. Smolka · 2017
Later among the works it cites.
HolStep : A machine learning dataset for higher order logic theorem proving
C. Kaliszyk, F. Chollet, and C. Szegedy · 2017
Later among the works it cites.
Progress in the independent certification of Mizar mathematical library in Isabelle
C. Kaliszyk and K. Pak · 2017
Later among the works it cites.
Making PVS accessible to generic services by interpretation in a universal format
M. Kohlhase, D. Müller, S. Owre, and F. Rabe · 2017
Later among the works it cites.
Formalization of the nominative algorithmic algebra in Mizar
A. Kornilowicz, A. Kryvolap, M. Nikitchenko, and I. Ivanov · 2017
Later among the works it cites.
Applying a formal method in industry: A 25-year trajectory
T. Lecomte, D. Deharbe, E. Prun, and E. Mottin · 2017
Later among the works it cites.
Formal modeling, analysis and verification of Black White Bakery algorithm
M. S. Nawaz, M. I. Lali, and S. Meng · 2017
Later among the works it cites.
POSTER: Towards precise and automated verification of security protocols in Coq
H. M. Palombo, H. Zheng, and J. Ligatti · 2017
Later among the works it cites.
QWIRE practice: Formal verification of quantum circuits in Coq
R. Rand, J. Paykin, and S. Zdancewic · 2017
Later among the works it cites.
Formal reasoning about systems biology using theorem proving
A. Rashid, O. Hasan, U. Siddique, and S. Tahar · 2017
Later among the works it cites.
Constraint solving for finite model finding in SMT solvers
A. Reynolds, C. Tinelli, and C. Barrett · 2017
Later among the works it cites.
The TPTP problem library and associated infrastructure - From CNF to TH0, TPTP v6.4.0
G. Sutcliffe · 2017
Later among the works it cites.
Formally verifying transfer functions of linear analog circuits
S. H. Taqdees and O. Hasan · 2017
Later among the works it cites.
A formalization of the process algebra CCS in HOL4
C. Tian · 2017
Later among the works it cites.
Formalized Lambek calculus in higher order logic (HOL4)
C. Tian · 2017
Later among the works it cites.
Formal verification: Will the seedling ever flower?
N. White, S. Matthews, and R. Chapman · 2017
Later among the works it cites.
Comparison of two theorem provers: Isabelle/HOL and Coq
A. Yushkovskiy · 2017
Later among the works it cites.
Towards verifying Ethereum smart contract bytecode in Isabelle/HOL
S. Amani, M. Bégel, M. Bortin, and M. Staples · 2018
Later among the works it cites.
Parallelizing SMT solving: Lazy decomposition and conciliation
X. Cheng, M. Zhou, X. Song, M. Gu, and J. Sun · 2018
Later among the works it cites.
Hammer for Coq: Automation for dependent type theory
L. Czajka and C. Kaliszyk · 2018
Later among the works it cites.
Coqoon - An IDE for interactive proof development in Coq
A. Faithfull, J. Bengtson, E. Tassi, and C. Tankink · 2018
Later among the works it cites.
Proofwatch: Watchlist guidance for large theories in E
Z. Goertzel, J. Jakubuv, S. Schulz, and J. Urban · 2018
Later among the works it cites.
Reinforcement learning of theorem proving
C. Kaliszyk, J. Urban, H. Michalewski, and M. Olsák · 2018
Later among the works it cites.
A formalization of metric spaces in HOL light
M. Maggesi · 2018
Later among the works it cites.
A formal design model for genetic algorithms operators and its encoding in PVS
M. S. Nawaz and M. Sun · 2018
Later among the works it cites.
Reo2PVS: Formal specification and verification of component connectors
M. S. Nawaz and M. Sun · 2018
Later among the works it cites.
Using PVS for modeling and verifying cloud services and their composition
M. S. Nawaz and M. Sun · 2018
Later among the works it cites.
The Boyer-Moore waterfall model revisited
P. Papapanagiotou and J. D. Fleuriot · 2018
Later among the works it cites.
A formal proof in Coq of a control function for the inverted pendulum
D. Rouhling · 2018
Later among the works it cites.
A library for combinational circuit verification using the HOL theorem prover
S. Shiraz and O. Hasan · 2018
Later among the works it cites.
Safe low-level code generation in Coq using monomorphization and monadification
A. Tanaka, R. Affeldt, and J. Garrigue · 2018
Later among the works it cites.
Verifying asymptotic time complexity of imperative programs in Isabelle
B. Zhan and M. P. L. Haslbeck · 2018
Later among the works it cites.
Theorem proving in Lean, release 3.4.0, 2019
J. Avigad, L. de Moura, and S. Kong · 2019
Closest in time.
Using PVS for modeling and verification of probabilistic connectors
M. S. Nawaz and M. Sun · 2019
Closest in time.
Proof guidance in PVS with sequential pattern mining
M. S. Nawaz, M. Sun, and P. Fournier-Viger · 2019
Closest in time.
Faster, higher, stronger: E 2.3
S. Schulz, S. Cruanes, and P. Vukmirovic · 2019
Closest in time.
Reasoning about connectors using Coq and Z3
X. Zhang, W. Hong, Y. Li, and M. Sun · 2019
Closest in time.