权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

高阶约束 Horn 子句：验证高阶程序的新方法

基本信息

批准号：
EP/T006579/1
负责人：
Luke Ong
金额：
$ 52.12万
依托单位：
University of Oxford
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2020
资助国家：
英国
起止时间：
2020 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FT006579%2F1
关键词：
Higher order Constrained Horn Clauses

项目摘要

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.

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