PV4 Cooperating Validity Checker (CVC3)produces a validity/satisfiability result for a formula

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula

Expected output

sat or unsat which indicates whether the SMT formula was satisfiable or not.

Comments

CVC3 is succeeded by CVC4 and cvc5.
SMT

Links

Related papers

CVC3 (CAV 2007)

Last publication date

2007

ProVerB specific

Markdown description: view/edit



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