BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automated Methods for Logic-Based Higher-Order Program Verificatio
 n - Hiroyuki Katsura (University of Cambridge)
DTSTART:20250527T120000Z
DTEND:20250527T130000Z
UID:TALK231091@talks.cam.ac.uk
CONTACT:Ariadne Si Suo
DESCRIPTION: This talk presents a robust framework for automated program v
 erification based on νHFL(T)\, a higher-order logic with greatest fixpoin
 ts modulo background theories. Leveraging its expressiveness\, νHFL(T) en
 ables a uniform and language-agnostic approach to automatically verifying 
 a wide range of properties\, such as the absence of pattern-matching failu
 res and out-of-bound array accesses\, across various programming languages
  including OCaml and Rust\, without requiring user-provided annotations. I
 t thus serves as a promising intermediate representation for fully automat
 ed verification. To fully realize this potential\, however\, a robust νHF
 L(T) solver is essential.\n\nIn this talk\, I will briefly introduce a set
  of automated methods developed during my PhD\, aimed at building such a s
 olver. Specifically\, we extend property-directed reachability to higher-o
 rder programs by introducing polymorphic refinement intersection types\, p
 ropose a testing-based falsification method using mode-guided program tran
 sformation\, and present a validity checking method based on the synthesis
  of catamorphisms for algebraic data types (ADTs). Each method has been im
 plemented and evaluated\, collectively enhancing the effectiveness and sca
 lability of νHFL(T)-based verification.
LOCATION:FS07\, Computer Laboratory
END:VEVENT
END:VCALENDAR