vcfloat
Floating-point verifier
A unified framework for verifying C programs with floating-point computations using Coq
VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations
24 stars
12 watching
11 forks
Language: Coq
last commit: 4 months ago
Linked from 2 awesome lists
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 thery/flocqlecture | An introductory course on formalizing floating-point numbers and their applications in Coq | 6 |
 certicoq/veriffi | Enables verified interaction between Coq programs and C libraries | 35 |
 bedrocksystems/brick | Formalization of C++ logic for verifying concurrent programming | 69 |
 vellvm/vellvm | A formal verification project of the LLVM compiler's semantics using Coq proof assistant. | 400 |
 verifytests/verify.brighter | Adds support for verifying a specific command processing framework | 2 |
 coq-community/coq-program-verification-template | A template project for verifying the correctness of C programs in Coq | 29 |
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 openhwgroup/cvfpu | A software framework for designing and generating floating-point processing units with transprecision capabilities | 437 |
 vrahli/velisarios | A framework for verifying the correctness of Byzantine fault-tolerant distributed systems | 28 |
 mit-pdos/perennial | A system for verifying correctness of concurrent and crash-safe systems with recovery procedures | 163 |
| coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 pirapira/evmverif | A framework for verifying smart contract code on the Ethereum Virtual Machine | 44 |
 ymherklotz/vericert | A tool for formally verifying high-level synthesis of digital circuits | 88 |
 smackers/smack | A software verification toolchain that translates C code into intermediate language and verifies its assertions using model checking and abstract interpretation | 431 |
 vcflib/vcflib | Provides methods to manipulate and interpret sequence variation described by the VCF format | 621 |