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.