-
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
