GitHub topics: compcert
AbsInt/CompCert
The CompCert formally-verified C compiler
Language: Coq - Size: 20.5 MB - Last synced at: 15 days ago - Pushed at: 24 days ago - Stars: 1,992 - Forks: 235
PrincetonUniversity/VST
Verified Software Toolchain
Language: Coq - Size: 74.9 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 463 - Forks: 94
INRIA/velus
A Lustre compiler in Coq
Language: Coq - Size: 9.76 MB - Last synced at: 15 days ago - Pushed at: 3 months ago - Stars: 70 - Forks: 6
CertiGraph/CertiGraph
A library for verifying graph-manipulating programs. Powered by Coq and VST. Compatible with CompCert.
Language: Coq - Size: 134 MB - Last synced at: 6 days ago - Pushed at: about 2 months ago - Stars: 18 - Forks: 6
appliedfm/docker-coq-vst
Docker images of the Coq proof assistant with compcert and VST pre-installed
Language: Shell - Size: 14.6 KB - Last synced at: 3 months ago - Pushed at: over 3 years ago - Stars: 4 - Forks: 0
appliedfm/coq-vsu-int63
Formally verified 63-bit integer arithmetic, implemented in C and proven in Coq
Language: Coq - Size: 146 KB - Last synced at: 2 months ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0
trommler/VeriGHC
Towards a verified back-end for The Glorious Glasgow Haskell Compilation System
Language: Coq - Size: 369 KB - Last synced at: 11 months ago - Pushed at: over 3 years ago - Stars: 8 - Forks: 2
appliedfm/coq-vsu
Tools for working with Verified Software Units
Language: OCaml - Size: 36.1 KB - Last synced at: 2 months ago - Pushed at: over 3 years ago - Stars: 1 - Forks: 0