Program
Verification
Book

PV4 ⊧ cvc4syproves unsatisfiability of a narrow class of formulae with counterexample-guided inductive synthesis

Application domain/field

Syntax-guided synthesis (SyGuS) solver
SMT solving

Type of tool

SyGuS solver

Expected input

SyGuS problem

Format:

SyGuS input format

Internals

cvc4sy is integrated in CVC4. cvc4sy is based on counterexample-guided inductive synthesis (CEGIS).

Comments

This solver specifically aims to prove unsatisfiability of formulae like:

\forall f \exists \bar{x} . \neg P [f, \bar{x}]

Links

CVC4 repository: https://github.com/CVC4/CVC4-archived/
Last commit date: 05 May 2021 (default branch)
Last commit date: 06 May 2021 (last activity)

Related papers

cvc4sy: Smart and Fast Term Enumeration for Syntax-Guided Synthesis

Last publication date

12 July 2019

Related tools

Other SyGuS solver: EUSolver

ProVerB specific

Markdown description: view/edit
Contained in the ProVerB22 dataset (paper + artefact)

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