The following projects use CVC4:
Boogie: A program verifier using the Boogie intermediate verification language. Supports CVC4 as a backend.
CIVL: A symbolic execution-based model checker for a dialect of C supporting concurrency. CVC4 is one of the backend provers.
CoSA: An SMT-based symbolic model checker for hardware design.
GPUVerify: A tool for formal static analysis of GPU kernels written in OpenCL and CUDA. It can prove that kernels are free from defects such as data races and barrier divergence. It is built on top of the Boogie verification engine, using CVC4 as one of the available theorem provers.
Inductor: A theorem prover for entailments between inductive definitions in first order and separation logics.
Inox (formerly Leon): A solver for higher-order functional programs. Supports CVC4 as a backend.
Isabelle (Sledgehammer): Isabelle is a generic proof assistant. Sledgehammer applies automated reasoning tools (including CVC4) to solve Isabelle subgoals.
Maude: A system supporting equational and rewriting logic specification and programming. Uses CVC4 as a backend.
Pysmt: A generic python interface for SMT solving. Supports CVC4 as a backend.
Rosette: A solver-aided programming language that extends Racket with language constructs for program synthesis and verification. Supports CVC4 as a backend solver.
SMTCoq: A Coq plugin that checks proof witnesses coming from external SAT and SMT solvers.
SPARK: SPARK is a verification paradigm for a subset of the Ada programming language. It uses CVC4 as the default backend for soving verification conditions.
Why3: A platform for deductive program verification. Uses CVC4 as an external prover.
Zelkova: Zelkova uses an encoding into the SMT theory of strings to check the security of access policies on Amazon Web Services.
If you use CVC4, please contact us and we’ll add your application here!