Third-Party Applications

The following projects use CVC4:

• Atelier B: An industrial tool enabling the operational use of the B Method to develop provably defect-free software. CVC4 is one of the backend provers.

• 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.

• Certora: Certora provides security analysis tools for Smart Contracts. The Certora Prover is capable of checking at compile-time that all executions of a Smart Contract fulfill a set of security rules. 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 solving verification conditions.

• Solc-Verify: An extended version of the Solidity compiler (v0.5.17) able to perform automated formal verification on Solidity smart contracts using specification annotations and modular program verification. CVC4 is one of the backend provers.

• Solidity’s SMTChecker: A built-in formal verification module in the Solidity Compiler. CVC4 is one of the backend provers.

• TorXakis: A model-based testing framework.

• 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!