Explore projects
-
SALVATI Sylvain / addition-lemma
MIT LicenseUpdated -
Updated
-
Attempt to gather different parts of a cylindrical decomposition algorithm as Coq-verified algorithms
Updated -
YUAN Shenghao / CertrBPF
GNU General Public License v2.0 or laterCertrBPF: a fully verified RIOT rBPF (verifier+interpreter+JIT) in Coq
Updated -
YUAN Shenghao / CertrBPFOpt
GNU General Public License v2.0 or laterUpdated -
Updated
-
Updated
-
CHARGUERAUD Arthur / cfml
X11 License Distribution Modification VariantUpdated -
CHARGUERAUD Arthur / cfml2
Creative Commons Attribution 4.0 InternationalSeparation Logic with Characteristic Formulae Entirely within Coq
Updated -
-
MOINE Alexandre / cfml-sek
MIT LicenseUpdated -
Updated
-
-
Updated
-
pred-tv / cohpred
GNU General Public License v3.0 or laterCoherent predicates: translation validation of properties of various types of predicates at runtime, interfacing with SMTCoq for validation of SMT unsatisfiability certificates.
Topics: CoqUpdated -
Providing comparison functions between numbers that are sums of a rational number and a square root, with proofs in Coq+mathematlcal components
Updated -
LECHENET Jean-Christophe / compcertssa
GNU Lesser General Public License v2.1 onlyCompCertSSA is built on top of the C CompCert verified compiler. It adds an SSA-based middle-end at the RTL level, and includes conversion to SSA, SSA-based optimizations, and destruction of SSA.
Updated -
CompCertSSA / compcertssa
GNU Lesser General Public License v2.1 onlyCompCertSSA is built on top of the C CompCert verified compiler. It adds an SSA-based middle-end at the RTL level, and includes conversion to SSA, SSA-based optimizations, and destruction of SSA.
Updated -
Gappa / coq
OtherA Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover.
Updated -
TASSI Enrico / coq
OtherA Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover.
Updated