PI: Steven Ramsay, University of Bristol, Co-Is: Eddie Jones, University of Bristol and Luke Ong, University of Oxford

  • Many pieces of critical software are written in functional programming languages, but the theory of higher-order program verification is challenging and applications are underdeveloped.
  • We designed the first really scalable pattern-match safety checker for Haskell, and used it to verify widely-used, open source Haskell libraries (POPL’21).
  • We laid the foundations of efficient equational reasoning using cyclic proof, in a system able to automatically prove correctness of functional programs with respect to equational specifications (PLDI’22).
  • We put higher-order program verification on a solid theoretical basis in higher-order logic (cf. first-order verification and first-order logic), through our development of higher-order MSL Horn clauses (POPL’23).
  • We are now working with the WhatsApp team at Meta to develop our work into scalable analyses for their Erlang codebases.

First-order program verification benefits enormously from a shared lexicon of notions of program invariant, such as inductive invariants and procedure summaries. In contrast, there are no generally accepted notions of invariant for higher-order verification. The goal of this studentship was to initiate the development of a theory of higher-order program invariants and of efficient algorithms for the automatic verification of functional programs.

The first outcome is a new compositional technique for formally verifying that a given functional program is free from pattern-match safety exceptions. Such exceptions can arise whenever a program does not handle all the cases that can arise in practice, such as data arriving in an unexpected format. Our analysis is guaranteed to scale linearly in program size, and we put it to work verifying large open-source Haskell packages in a few hundred milliseconds.

One of the advantages of (pure) functional programming is that useful specifications can written only using equations between program expressions. Then automatic verification requires means to reason about equations inductively. The second outcome is to lay the foundations of efficient, inductive equational reasoning using cyclic proof. We designed an elegant but efficient calculus, developed the underlying theory and built prototype tool that can verify equational specifications of Haskell functions.

The third outcome is a new foundation for higher-order program verification. Our development of a higher-order extension to MSL Horn constraints shows how various technologies for higher-order program verification can be located in a unifying conceptual landscape based on higher-order logic and resolution. We demonstrated the advantages of this view by developing a library for verified socket programming in Haskell.

PUBLICATIONS. [1] E. Jones and S. Ramsay. 2021. “Intensional datatype refinement with application to scalable verification of pattern-match safety”. POPL 21.  [2] E Jones, C-H L Ong and S Ramsay.  “CycleQ: an efficient basis for cyclic equational reasoning”. PLDI 2022. [3] J Jochems, E Jones and S Ramsay. “Higher-order MSL constraints”. POPL 2023.

RELATED GRANTS.  Higher-order Constrained Horn Clauses: A New Approach to Verifying Higher-order Programs” (EPSRC EP/T006595/1, £366k).  “Scalable, Static Taint Analysis for Core Erlang” (Meta Research Award)

IMPACT. Our tool is packaged as a GHC plugin and available on the Hackage package repository. It has been used to verify that a number of widely-used, open-source Haskell libraries (such as aeson, containers, and time) are free from pattern-match safety exceptions.

“Techniques for automatically analysing higher-order functional programs are potentially very useful to WhatsApp, which is home to one of the biggest Erlang codebases. In the coming year, we will be working with the authors on transferring their foundational work into something that can have real impact on some of the technical challenges we face at Meta.” – Ákos Hajdu, Software Engineer at Meta, working on the WhatsApp team.