-
Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq
In this thesis, we propose new automation capabilities for the Coq proof assistant. We obtain this mechanization via an integration into Coq of decision procedures for... -
Harnessing SMT Solvers for TLA+ Proofs
International audience -
Semi-automatic verification of cryptographic primitives
CertiCrypt is a framework that enables the machine-checked construction and verification of cryptographic proofs in the Coq proof assistant. CertiCrypt instruments the... -
Two simulations about DPLL(T)
In this paper we relate different formulations of the DPLL(T ) procedure. The first formulation is based on a system of rewrite rules, which we denote DPLL(T ). The... -
Modular Instantiation Schemes
International audience
