PV4 ⊧ GSpacerproduces a satisfiability result for a given CHC

Application domain/field

• SMT solving
• CHC solving

Type of tool

CHC solver

Expected output

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

Internals

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