cvc5
Satisfiability checker
An open-source tool for determining the satisfiability of first-order formulas modulo theories.
cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.
1k stars
36 watching
236 forks
Language: SMT
last commit: 3 months ago
Linked from 1 awesome list
aolofsson/awesome-opensource-hardwareRelated projects:
| Repository | Description | Stars |
|---|---|---|
 d-m-bailey/cvc | Checks CDL netlists for errors and circuit validity | 22 |
 leventerkok/sbv | A tool for expressing and proving properties about Haskell programs using SMT solvers. | 245 |
 cvxr/tfocs | A toolbox for building efficient first-order solvers for convex optimization problems | 136 |
 princetonuniversity/vst | A collection of formal verification tools and libraries for writing secure and reliable software using the Coq proof assistant | 444 |
 valeevgroup/mpqc | A program for ab initio simulation of the electronic structure of molecules and periodic solids using the time independent Schrödinger equation. | 68 |
 smtcoq/smtcoq | An OCaml-based plugin for Coq that verifies and extends proof witnesses from external SAT/SMT solvers | 157 |
 scottybauer/android_kernel_cve_pocs | A collection of C programs demonstrating proof-of-concept vulnerabilities in Android. | 674 |
 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 |
 verifytests/verify.communitytoolkit.mvvm | A test suite for verifying the behavior of CommunityToolkit.Mvvm | 1 |
 coq-community/comp-dec-modal | Machine-checked proofs of soundness, completeness, and decidability for modal logics in Coq. | 8 |
 diffblue/cbmc | A tool for verifying the correctness and safety of C++ programs | 863 |
 ymherklotz/vericert | A tool for formally verifying high-level synthesis of digital circuits | 88 |
 symbioticeda/riscv-formal | A framework for formally verifying RISC-V processors by providing a processor-independent formal description and testbenches. | 589 |
 smackers/smack | A software verification toolchain that translates C code into intermediate language and verifies its assertions using model checking and abstract interpretation | 431 |
 golyshkin/vectordbcchecker | An application for checking DBC files for various issues and extending checker functionality. | 4 |