Program
Verification
Book

PV4 ⊧ cvc5produces a satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Format:

Expected output

sat or unsat

Internals

cvc5 can be used as a stand-alone tool or as a library. There is an API available for C++, Java and Python.

Links

Repository: https://github.com/cvc5/cvc5
- Last commit date: 26 February 2023 (default branch)
- Last commit date: 26 February 2023 (last activity)
Project page: https://cvc5.github.io/

Related papers

Even Fast Conflicts and Lazier Reductions for String Solvers (CAV 2022)
cvc5: A Versatile and Industrial-Strength SMT Solver (TACAS 2022)
Bit-Precise Reasoning via Int-Blasting (VMCAI 2022)

Last publication date

2022

Related tools

From the same 'family' of tools: CVC, CVC Lite, CVC3, CVC4

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.