Master's Thesis in Computer Science: Verification of the Blocking and Non-Blocking Michael-Scott Queue Algorithms
-
Updated
May 29, 2024 - TeX
Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs. Typical
applications include the certification of properties of programming languages,
the formalization of mathematics and teaching.
Master's Thesis in Computer Science: Verification of the Blocking and Non-Blocking Michael-Scott Queue Algorithms
Probabilistic separation logics for verifying higher-order probabilistic programs.
Visual Studio Code Extension and Language Server Protocol for Coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for RISC-V with focus on a formally verified and auditable security monitor.
Índice de repositorios.
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
A verification toolchain for Rust programs
Check 100% of execution cases of Rust programs 🦀 to make applications with no bugs!
Formalization of C++ for verification purposes.
Readings on computational logic, interactive theorem proving and functional programming.
A function definition package for Coq
Ring, field, lra, nra, and psatz tactics for Mathematical Components
Micromega tactics for Mathematical Components
Some personal notes on typical algebra topics
A Verified Compiler for Gallina, Written in Gallina
Created by Gérard Pierre Huet, Thierry Coquand
Released 1989
Latest release 3 months ago