Automated Methods for Logic-Based Higher-Order Program Verification

Add to your list(s) Download to your calendar using vCal

• Hiroyuki Katsura (University of Cambridge)
• Tuesday 27 May 2025, 13:00-14:00
• FS07, Computer Laboratory.

If you have a question about this talk, please contact Ariadne Si Suo .

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.

This talk is part of the SANDWICH Seminar (Computer Laboratory) series.

This talk is included in these lists:

• FS07, Computer Laboratory
• tcw57’s list

Note that ex-directory lists are not shown.