Sciweavers

ITP
2010
163views Mathematics» more  ITP 2010»
13 years 7 months ago
Fast LCF-Style Proof Reconstruction for Z3
Abstract. The Satisfiability Modulo Theories (SMT) solver Z3 can generate proofs of unsatisfiability. We present independent reconstruction of these proofs in the theorem provers...
Sascha Böhme, Tjark Weber
ITP
2010
159views Mathematics» more  ITP 2010»
13 years 7 months ago
Programming Language Techniques for Cryptographic Proofs
CertiCrypt is a general framework to certify the security of cryptographic primitives in the Coq proof assistant. CertiCrypt adopts the code-based paradigm, in which the statement ...
Gilles Barthe, Benjamin Grégoire, Santiago ...