This repository contains some nuHFL(Z) (aka higher-order CHC) solvers, a fixpoint logic for higher-order program verification:
- HoPDR: A higher-order extension of Property-Directed Reachability
- ModeTrans: A testing framework for disproving fixpoint logic formulas with mode-guided transformation to functional programs
%HES
𝒞₁;
𝒞₂;
⋮
𝒞ₙ;
where 𝒞₁ is the top-level formula and
atom := false | true | n
φ := atom | x | φ₁ <op> φ₂ | φ₁ <pred> φ₂ | φ₁ \/ φ₂ | φ₁ /\ φ₂ | φ₁ t | φ₁ φ₂ | ∀x. φ | \x. φ
𝒞 := X x₁ ⋯ xₙ =v φ
op := + | - | *
pred := < | <= | > | >= | != | =
- See .github/workflows/test.yaml and hopdr/docker/Dockerfile for the detail
cargo run --release --bin hopdr
hopdr --input <filename>
In addition to the above syntax, you can input SMT2Lib CHCs with the option --chc.
- Ultimate Eliminator
- Z3
- ocamlopt
- ocamlformat
cargo run --release --bin check
check --input <filename>
Artifact (docker image) for APLAS24 is available at zenodo.