-
Automated verification of termination certificates
National 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... -
Design and implementation of a proof verifying kernel for the λΠ-calculus modulo
In recent years, the emergence of feature rich and mature interactive proof assistants has enabled large formalization efforts of high-profile conjectures and results... -
Kleene algebra, Rewriting modulo AC and Circuits in Coq.
This thesis describe three formalisations in Coq. The first chapter is devoted to the implementation of an efficient decision procedure for Kleene algebras : as... -
Generating formally certified bounds on values and round-off errors
International audience -
Formal Verification of Hardware Synthesis
International audience -
Formalized algebraic numbers: construction and first-order theory.
This thesis presents a formalization of algebraic numbers and their theory. It brings two new important contributions to the formalization of mathematical results in... -
A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
International audience -
From Tarski to Hilbert
International audience -
A formal framework for model verification in System Engineering: UPSL
The aim of this paper is to present and to illustrate a formal model verification framework called UPSL (Unified Property Specification Language) applied here in... -
Theorem of three circles in Coq
25 pages, 5 figures -
Formal verification of a software countermeasure against instruction skip att...
16 pages. Please contact the authors to get the pre-proceedings version. -
Dependability assessment of large railway systems
International audience -
A Formal Proof of Countermeasures Against Fault Injection Attacks on CRT-RSA
International audience -
Interaction between linear algebra and analysis in formal mathematics
In this thesis we present the formalization of three principal results that are the Jordan normal form of a matrix, the Bolzano-Weierstraß theorem, and the... -
A Vernacular for Coherent Logic
International audience -
Formal Analysis of CRT-RSA Vigilant's Countermeasure Against the BellCoRe Att...
International audience -
Accurate Summation: Towards a Simpler and Formal Proof
Colloque avec actes et comité de lecture. internationale. -
Toward the Integration of Numerical Computations into the OMSCS Framework
Colloque avec actes et comité de lecture. internationale.
