PI: Steven Ramsay, University of Bristol, Co-I: Luke Ong, University of Oxford
- Higher-order programming is gaining traction, especially in financial and scientific industries.
- There is no consensus around a mathematical foundation for higher-order program verification.
- We propose higher-order constrained Horn clauses as a unifying logical paradigm.
- We look to exploit logical techniques to provide practical program verification technologies.
- We presented a highly efficient pattern-match safety analysis based on logical resolution and verified a number of widely-used, open source Haskell libraries.
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 in the higher-order verification literature. The goal of this studentship is to initiate the development of a unifying theory of higher-order program invariants. A theory which can express the common, logical underpinnings of the subject and yet supports effective and reusable automated reasoning tools.
In the last year, we have developed a new compositional reasoning technique for formally verifying that a given functional program is free from pattern-match safety exceptions, based on a restricted form of logical resolution. 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 or when a defective component interacts using a wider variety of actions than are advertised in its protocol.
The technique is designed to be lightweight and usable by the average programmer. Our prototype tool is fully automatic, but we have avoided the “push a button and hope for the best” user-experience that can hinder adoption by giving strong guarantees on predictability:
– compositionality ensures the running time of our analysis scales linearly in the size of the analysed program and, in practice, large Haskell packages can be verified in a few hundred milliseconds.
– the power of the analysis is characterised by an intuitive extension of the Haskell type system, so programmers are readily able to understand why a component may not be verifiable.
PUBLICATIONS. E. Jones and S. Ramsay. 2021. “Intensional datatype refinement with application to scalable verification of pattern-match safety”. POPL 21.
RELATED GRANTS. Higher-order Constrained Horn Clauses: A New Approach to Verifying Higher-order Programs. (EPSRC EP/T006595/1).
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.