6 datasets found

CertiCrypt is a framework that enables the machine-checked construction and verification of cryptographic proofs in the Coq proof assistant. CertiCrypt instruments the...

Parallel program design and implementation is a complex, error prone task. Verifying parallel programs is also harder than verifying sequential ones. To ease the...

This thesis belongs to the domain of software verification. The goalof verifying software is to ensure that an implementation, a program,satisfies the requirements,...

This thesis presents an algorithm that eliminates square root and division operations in some straight-line programs used in embedded systems while preserving the...

National audience

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...