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

Internals

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

Links

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

Last commit date

19 December 2019

Related papers

https://doi.org/10.1007/978-3-030-53291-8_7

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



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