Program
Verification
Book

PV4 ⊧ Spacerproduces a satisfiability result for Constrained Horn Clauses

Solver for Constrained Horn Clauses (CHC), implemented in Z3

Application domain/field

Constrained Horn Clauses
CHC solver

Type of tool

CHC solver

Internals

RECMC

Comments

Integrated in Z3.

Related papers

SMT-based model checking for recursive programs (Formal Methods in System Design '16)
SMT-Based Model Checking for Recursive Programs (CAV '14)

Related tools

GSpacer: Extension of Spacer

ProVerB specific

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

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