Higher-Order Program Verification

Catalia: Solver for Constrained Horn Clauses over Algebraic Data Types

This is a tool to convert HORS(Z) model checking problems to HFL(Z) represented as Rocq code, as described in the paper: https://dl.acm.org/doi/10.1145/3294032.3294077

An ICE-based predicate synthesizer for Horn clauses.

Simple Craig interpolants for linear integer arithmetic

OCaml library for manipulaing HFL formulas

ReTHFL: νHFL(Z) (aka higher-order CHC) solver based on refinement types

Nola: Later-Free Ghost State for Verifying Termination in Iris

MoCHi: Model Checker for Higher-Order Programs

counter-example guided based verifier for hflz