PV4 GSpacerproduces a satisfiability result for a given CHC

Application domain/field

Type of tool

CHC solver

Expected output

safe (and an inductive invariant so that the system can be proven to be safe) or unsafe


Extension of Spacer, a CHC (Constrained Horn Clause) solver in Z3, with global guidance (to tackle limitations of locality).


Repository: https://github.com/hgvk94/z3/tree/gspacer-cav-ae

Related papers

Global Guidance for Local Generalization in Model Checking

Last publication date

14 July 2020

ProVerB specific

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