PV4 FreqHornproves satisfiability of a CHC system by generating invariants

Application domain/field

Type of tool

CHC solver

Expected output

Either an invariant or false if no invariant exists

Internals

FreqHorn is a satisfiability solver for constrained Horn clauses (CHCs). Uses Z3 to filter candidates, based on SeaHorn.
CHC SyGuS

Links

Last commit date

11 June 2021

Related papers

Last publication date

12 July 2019

ProVerB specific

View/edit source (Markdown)



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