vericert
HLS verifier
A tool for formally verifying high-level synthesis of digital circuits
A formally verified high-level synthesis tool based on CompCert and written in Coq.
88 stars
12 watching
5 forks
Language: Coq
last commit: 5 months ago coqhigh-level-synthesis
Related projects:
| Repository | Description | Stars |
|---|---|---|
 jscert/jscert | A Coq-based verification of the ECMAScript 5 standard for a JavaScript interpreter | 196 |
 certigraph/certigraph | A verification toolset for graph-manipulating programs written in Coq. | 17 |
 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 |
 uwplse/verdi | A framework for formally verifying distributed systems implementations in Coq. | 589 |
 xilinx/hls | A collection of tools and code for designing and implementing digital circuits using high-level synthesis | 379 |
 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 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 442 |
 mit-pdos/perennial | A system for verifying correctness of concurrent and crash-safe systems with recovery procedures | 163 |
 ucsd-progsys/liquidhaskell | A tool for verifying and validating Haskell programs using refinement types and SMT logic | 1,196 |
 josefgit/concert | A framework for verifying smart contracts in Coq, a proof assistant language. | 0 |
 bedrocksystems/brick | Formalization of C++ logic for verifying concurrent programming | 69 |
 vrahli/velisarios | A framework for verifying the correctness of Byzantine fault-tolerant distributed systems | 28 |
 siimplex/concert | A framework for verifying smart contracts in Coq | 1 |
 thery/coqprime | A proof assistant library for prime number certification using elliptic curves and Pocklington certificates | 37 |
 veridise/picus | Automated tool for verifying uniqueness properties in zero-knowledge proof circuits | 70 |