EPSRC logo

Details of Grant 

EPSRC Reference: EP/T006579/1
Title: Higher-order Constrained Horn Clauses: A New Approach to Verifying Higher-order Programs
Principal Investigator: Ong, Professor CHL
Other Investigators:
Murawski, Dr A
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: University of Oxford
Scheme: Standard Research
Starts: 01 September 2019 Ends: 31 August 2022 Value (£): 409,019
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
EP/T006595/1
Panel History:
Panel DatePanel NameOutcome
10 Jul 2019 EPSRC ICT Prioritisation Panel July 2019 Announced
Summary on Grant Application Form
The construction of bug-free programs is a challenging research problem of international importance and huge potential impact. Yet the traditional approaches to achieving confidence in software, such as testing and debugging, are not effective, often accounting for 50-75% of the total development cost.

This project is about a new approach to the verification of higher-order functional programs. Functional programs have long been applied to real-world tasks. Programmers use functional languages because they can build more robust code more quickly and with fewer errors than they could before, thereby boosting reliability and cutting costs. Others turn to functional languages because of the advantages they offer in data parallelism, concurrency, GPGPU and cloud programming.

Thus by making functional programming safer and more robust and productive, techniques and tool support for the formal analysis of functional programs will bring significant benefits to the digital economy as a whole, but especially to financial modelling, scientific applications, computing and telecommunications, which are vital to current and future UK economic success.

Higher-order model checking and refinement type inference are currently the two leading approaches to fully automatic verification of higher-order programs. However, the technologies are rather different and their relative strengths are not well understood.

This project aims to develop a new approach to the verification of higher-order programs based on HIGHER-ORDER CONSTRAINED HORN CLAUSES. A recent innovation in symbolic model checking, Horn constraints exploit the successful combination of automated deduction technologies with the satisfiability checking of formulas. Our verification method will be automatic and programming-language independent.

In contrast to model checking and refinement type inference, by adopting higher-order constrained Horn clauses--a fragment of higher-order logic--as the common formalism for expressing verification problems, this approach to verification has a number of ADVANTAGES:

(i) It enables a separation of concerns: verification engineers (users of the verification framework) need only concern themselves with generating verification conditions and the attendant specificities of programming languages, whilst the "symbolic model checking" is kept purely logical and hence generic; the implementation of the backend engine is left to the experts in automated deduction and algorithmic verification.

(ii) It promotes benchmarking of software model checking tools.

(iii) It fosters extensibility and retargetability of tool chains.

Our HYPOTHESIS is that the higher-order Horn constraint framework is well-founded, expressive, efficient, and convenient to use.

Building on our recent and preliminary work, our OBJECTIVES are as follows.

(i) Establish HoCHC as a robust fragment of higher-order logic, algorithmically and semantically.

(ii) Develop HoCHC into a comprehensive verification framework to rival established approaches.

(iii) Design efficient algorithms for solving HoCHC decision problems.

To evaluate the ease-of-use and efficiency of the approach, we will conduct case studies involving Haskell libraries and Wolfram Mathematica code.

Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.ox.ac.uk