Program
Verification
Book

PV4 ⊧ FreqHornproves satisfiability of a CHC system by generating invariants

Application domain/field

Constrained Horn Clause (CHC) solver
Invariant synthesis
Syntax-guided synthesis (SyGuS)

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.

Links

Repository: https://github.com/freqhorn/freqhorn
- Last commit date: 09 Aug 2022 (default branch)
- Last commit date: 26 Nov 2022 (last activity)
Other repository that is also linked: https://github.com/grigoryfedyukovich/aeval/tree/rnd
- Last commit date: 09 Aug 2022 (default branch)

Related papers

Quantified Invariants via Syntax-Guided Synthesis (CAV '19)
Solving Constrained Horn Clauses Using Syntax and Data (FMCAD '18)

Last publication date

12 July 2019

ProVerB specific

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

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