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

构建无bug程序是一个具有国际重要性和巨大潜在影响的具有挑战性的研究问题。然而，在软件中实现信心的传统方法，如测试和调试，并不有效，通常占总开发成本的50-75%。这个项目是关于验证高阶函数程序的一种新方法。函数式程序长期以来一直应用于现实世界的任务。程序员使用函数式语言是因为他们可以比以前更快地构建更健壮的代码，并且错误更少，从而提高可靠性并降低成本。其他人则转向函数式语言，因为它们在数据并行性、并发性、GPGPU和云编程方面具有优势。因此，通过使函数式编程更安全、更健壮、更高效，对函数式程序形式分析的技术和工具支持将为整个数字经济带来显著的好处，尤其是对金融建模、科学应用、计算和电信，这些对当前和未来的英国经济成功至关重要。高阶模型检查和精化类型推断是目前实现高阶程序全自动验证的两种主要方法。然而，这些技术差别很大，它们的相对优势还没有得到很好的理解。本项目旨在开发一种基于高阶约束HORN子句的高阶程序验证新方法。符号模型检查的最新创新，霍恩约束利用了自动演绎技术与公式的可满足性检查的成功结合。我们的验证方法将是自动的和独立于编程语言的。与模型检查和优化类型推断相比，通过采用高阶约束的Horn子句（高阶逻辑的片段）作为表达验证问题的常见形式，这种验证方法具有许多优点：(i)它可以分离关注点：验证工程师（验证框架的用户）只需要关注生成验证条件和随之而来的编程语言的特殊性，而“符号模型检查”则保持纯逻辑，因此是通用的；后端引擎的实现留给了自动推理和算法验证方面的专家。（ii）促进软件模型检查工具的基准测试。（iii）促进工具链的可扩展性和可重定向性。我们的假设是，高阶霍恩约束框架是有充分基础的、富有表现力的、高效的和方便使用的。基于我们最近和初步的工作，我们的目标如下。(i)在算法和语义上将HoCHC建立为高阶逻辑的鲁棒片段。（ii）将医院健康中心发展成一个全面的核查框架，与现有的方法相抗衡。（iii）设计求解HoCHC决策问题的高效算法。为了评估该方法的易用性和效率，我们将进行涉及Haskell库和Wolfram Mathematica代码的案例研究。

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.