coq-program-verification-template
C verifier
A template project for verifying the correctness of C programs in Coq
Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]
29 stars
3 watching
2 forks
Language: Coq
last commit: 4 months ago coqprogram-verificationtemplatetemplate-repository
Related projects:
| Repository | Description | Stars |
|---|---|---|
| coq-community/templates | Provides template files for generating configuration and boilerplate for Coq projects | 13 |
 certicoq/veriffi | Enables verified interaction between Coq programs and C libraries | 35 |
| coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 certigraph/certigraph | A verification toolset for graph-manipulating programs written in Coq. | 17 |
| 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 |
 bedrocksystems/brick | Formalization of C++ logic for verifying concurrent programming | 69 |
 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/paramcoq | A Coq plugin providing commands for generating parametricity statements used in data refinement proofs. | 44 |
 formal-land/coq-of-python | Formal verification of Python code using Coq | 30 |
 huynhtrankhanh/coqcp | Verifying competitive programming solutions to catch errors and improve rigor through formal mathematical proof | 22 |
| coq-community/lemma-overloading | A Coq library demonstrating design patterns for automated proof automation and canonical structures | 26 |
 absint/compcert | A formally verified C compiler with guaranteed correct assembly code generation | 1,888 |
| coq-community/reglang | Provides definitions and verified translations between various representations of regular languages in the Coq proof assistant | 41 |
| coq-community/coq-ext-lib | A collection of reusable Coq definitions and theorems for building software development tools | 129 |