CompCert
C compiler
A formally verified compiler for a subset of C that generates code for multiple architectures.
The CompCert formally-verified C compiler
2k stars
63 watching
230 forks
Language: Coq
last commit: about 1 month ago ccompcertcompilercoq
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. | 137 |
 pa-ba/calc-comp | Formalizations of compiler design and virtual machine calculations in Coq | 30 |
 inria/velus | A formally verified compiler for the Lustre programming language | 63 |
 jscert/jscert | A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter | 196 |
 sigurdschneider/lvc | A compiler project that aims to formalize and verify the semantics of an intermediate language using Coq | 57 |
| certicoq/veriffi | Enables verified interaction between Coq programs and C libraries | 39 |
 l1mey112/crepl | A compiler and interpreter for executing C code on the fly as it is typed. | 29 |
 hackerfoo/poprc | A compiler for a language that supports recursion and concatenative data structures with features like dependent types and partial evaluation | 244 |
 c2lang/c2compiler | A C compiler written in the C2 language itself. | 703 |
 jserv/amacc | A compiler for the Arm architecture that compiles a subset of C to generate executables and supports just-in-time execution. | 1,018 |
 cpitclaudel/company-coq | An Emacs plugin that enhances Coq mode with various features and tools for writing and debugging proof-based software | 351 |
 vexu/arocc | A compiler written in Zig to translate C code into machine-specific binary code | 1,151 |
 querycert/qcert | A framework for developing and verifying domain-specific languages with a focus on compiler correctness and verification. | 56 |