Higher-order Constrained Horn Clauses: A New Approach to Verifying Higher-order Programs

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.

SCIENTIFIC COMMUNITY: KNOWLEDGE CREATION

The proposed research concerns new foundations, algorithms and tools for finding bugs in functional programs (such as F#, Haskell, OCaml, Scala and Erlang) or otherwise showing their absence. The work will impact the scientific community because of the new knowledge that will be created. It will impact on and benefit the academics and researchers working in the following areas:

A. Verification and Correctness

B. Programming Languages

C. Theory of Computing, especially Logic and Algorithms, Games, and Lambda Calculus and Types

In the medium term, there is a clear path from the proposed research to industrial-strength tooling that helps to manage the safety and security risks posed by implementation bugs - a path which has, in part, already been followed successfully for underpinning work on first-order imperative programs (such as C). Consequently, the research directly addresses the cross-ICT priority Safe and Secure ICT and makes potentially strong contributions towards the prosperity outcomes Resilient Nation (Ambition R3) and Connected Nation (Ambition C4).

FINANCIAL MODELLING, SCIENTIFIC APPLICATIONS, COMPUTING AND TELECOMMUNICATIONS: SAFER AND MORE ROBUST CODE

In terms of the strategic themes identified by EPSRC, this proposal sits most naturally with the DIGITAL ECONOMY theme (in particular, with the CLOUD COMPUTING, and VALUE CREATION AND CAPTURE subthemes - see (ii) and (iii) below, respectively).

The construction of bug-free programs is a challenging research problem of international importance and huge potential impact. In a National Institute of Standards and Technology report of 2002, the cost to the US economy of faulty software was estimated at $60 billion. It is vitally important to transfer the benefits of automatic verification techniques to higher-order functional languages such as F#, OCaml, Haskell and Erlang.

(i) Higher-order constructs such as first-class functions, lambda-expressions and closures are now basic features of the most widely-used languages such as Javascript, Perl5, Python, C# and C++0x, which are standard in web programming, hardware and embedded systems design.

(ii) Because functional languages support domain-specific languages and are good for organising data parallelism, they are widely used in scientific applications and financial modelling.

(iii) The absence of mutable variables and the use of monadic structuring principle to encapsulate side-effects make functional languages attractive for concurrent programming, which has become extremely important thanks to the rapid growth of multi-core and GPGPU processing and cloud computing.

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 financial modelling, scientific applications, and the computing and telecommunications industries, which are vital to current and future UK economic success.

WEALTH CREATION

The development of verification techniques and tools is an important precursor to wealth creation because of the opportunities for licensing and spin-offs. Indirectly all of society will benefit because they give rise to safe and reliable software. Our daily lives rely on software infrastructure for banking, communications, travel, shopping, and many other necessities. Ultimately better verification techniques and tools for software will lead to better quality of life in the digital world.