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

Application domain/field

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: fx¯.¬P[f,x¯]
SAT SyGuS

Links

CVC4 repository: https://github.com/CVC4/CVC4-archived/

Last commit date

17 June 2020 (=> most recent commit with 'sygus' in commit message)

Related papers

https://doi.org/10.1007/978-3-030-25543-5_5

Last publication date

12 July 2019

Related tools

Other SyGuS solver: EUSolver

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.