Predicate Abstraction and CEGAR for nuHFL(Z) Validity Checking
summary
Proposes an algorithm that combines νHFL(ℤ) predicate abstraction with predicate abstraction and CEGAR to decide higher‑order CHC/νHFL(ℤ) validity, implements a checker, and proves soundness, completeness w.r.t. refinement intersection type and a CEGAR progress property (no counterexample repeats). Handles tree‑shaped counterexamples and abstracts integers to booleans. Evaluation: the tool solves more benchmarks than Horus (Horus is faster on successes) and is competitive with MoCHi on runtime while solving fewer problems; the implementation works but is slower.
AI-written summary · about