CertiGraph
Graph verifier
A verification toolset for graph-manipulating programs written in Coq.
A library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.
17 stars
10 watching
5 forks
Language: Coq
last commit: 3 months ago
Linked from 1 awesome list
compcertcoqgraph-algorithmsvst
Related projects:
| Repository | Description | Stars |
|---|---|---|
 verifid/graph-vl | An identity verification system with GraphQL and Postgres database | 60 |
 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 | 39 |
 josefgit/concert | A framework for verifying smart contracts in Coq, a proof assistant language. | 0 |
 ymherklotz/vericert | A tool for formally verifying high-level synthesis of digital circuits | 88 |
 frederikvigen/concert | A framework for verifying smart contracts in Coq to ensure their correctness and security | 0 |
| 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. | 137 |
 easycrypt/certicrypt | A framework for formal verification and validation of cryptographic proofs using Coq | 33 |
| coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 jscert/jscert | A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter | 196 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
 verifytests/verify.serilog | A tool for verifying Serilog logging behavior in C# applications | 1 |
| coq-community/graph-theory | Formalized graph theory results for research and verification | 35 |
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 certikos/coqrel | A Coq-based library for establishing logical relations in formal verification and proof assistance | 20 |