BRiCk
C++ verifier
Formalization of C++ logic for verifying concurrent programming
Formalization of C++ for verification purposes.
69 stars
6 watching
10 forks
Language: Coq
last commit: 10 days ago coqcoq-formalizationcoq-librarycpluspluscplusplus-11cplusplus-14cplusplus-17
Related projects:
| Repository | Description | Stars |
|---|---|---|
 mit-plv/bedrock | Automated verification of higher-order programs using separation logic | 57 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |
 formal-land/coq-of-rust | Tool that verifies Rust code by translating it into Coq's proof system to ensure no bugs or vulnerabilities exist | 421 |
 coq-community/coq-program-verification-template | A template project for verifying the correctness of C programs in Coq | 29 |
 certicoq/veriffi | Enables verified interaction between Coq programs and C libraries | 35 |
 rafaelcgs10/w-in-coq | A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools. | 25 |
 verifytests/verify.moq | Adds Verify support for Moq types to verify mock behavior and assertions | 14 |
 mit-pdos/perennial | A system for verifying correctness of concurrent and crash-safe systems with recovery procedures | 163 |
| formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
| verifytests/verify.brighter | Adds support for verifying a specific command processing framework | 2 |
 jscert/jscert | A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter | 196 |
| coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 smackers/smack | A software verification toolchain that translates C code into intermediate language and verifies its assertions using model checking and abstract interpretation | 431 |
 imdea-software/fcsl-pcm | Provides formalisation of Partial Commutative Monoids (PCMs) for verification of pointer-manipulating sequential and concurrent programs. | 26 |