VeriFFI
Verification library
Enables verified interaction between Coq programs and C libraries
VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project
35 stars
8 watching
2 forks
Language: Coq
last commit: 4 months ago Related projects:
| Repository | Description | Stars |
|---|---|---|
| certicoq/certicoq | A compiler for a subset of the C language that can be compiled with any standard C compiler, used in formal verification and proof assistance. | 136 |
 coq-community/coq-program-verification-template | A template project for verifying the correctness of C programs in Coq | 29 |
 certigraph/certigraph | A verification toolset for graph-manipulating programs written in Coq. | 17 |
 bedrocksystems/brick | Formalization of C++ logic for verifying concurrent programming | 69 |
 verifytests/verify.brighter | Adds support for verifying a specific command processing framework | 2 |
| coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |
 absint/compcert | A formally verified C compiler with guaranteed correct assembly code generation | 1,888 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |
 jscert/jscert | A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter | 196 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| verifytests/verify.moq | Adds Verify support for Moq types to verify mock behavior and assertions | 14 |
 jwiegley/coq-haskell | A Coq library providing definitions and notations to facilitate interaction between Haskell developers and the Coq proof assistant. | 167 |
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |