Abstract

This talk presents a robust framework for automated program verification based on νHFL(T), a higher-order logic with greatest fixpoints modulo background theories. Leveraging its expressiveness, νHFL(T) enables a uniform and language-agnostic approach to automatically verifying a wide range of properties, such as the absence of pattern-matching failures and out-of-bound array accesses, across various programming languages including OCaml and Rust, without requiring user-provided annotations. It thus serves as a promising intermediate representation for fully automated verification. To fully realize this potential, however, a robust νHFL(T) solver is essential.

In this talk, I will briefly introduce a set of automated methods developed during my PhD, aimed at building such a solver. Specifically, we extend property-directed reachability to higher-order programs by introducing polymorphic refinement intersection types, propose a testing-based falsification method using mode-guided program transformation, and present a validity checking method based on the synthesis of catamorphisms for algebraic data types (ADTs). Each method has been implemented and evaluated, collectively enhancing the effectiveness and scalability of νHFL(T)-based verification.