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

GitHub

24 stars

12 watching

11 forks

Language: Coq

last commit: 7 months ago

Linked from 2 awesome lists

Backlinks from these awesome lists:

Related projects:

Repository	Description	Stars
thery/flocqlecture	An introductory course on floating-point numbers and formal proof using Coq	6
certicoq/veriffi	Enables verified interaction between Coq programs and C libraries	39
vellvm/vellvm	A formal verification project of the LLVM compiler's semantics using Coq proof assistant.	405
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 flexible and parameterizable floating-point unit design for RISC-V processors	440
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	165
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	A C++ library and command-line tools for parsing, manipulating, and analyzing VCF files used in genomics and bioinformatics.	628