Expressivity and Algorithmics of Higher-Order Horn Clauses

高阶 Horn 子句的表达性和算法

• 批准号: 1893570
• 金额: --
• 依托单位: University of Oxford
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2017
• 资助国家: 英国
• 起止时间: 2017 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-1893570
• 关键词: Expressivity; Algorithmics; Higher; Order; Horn

This project falls within the EPSRC Verification and Correctness research areaAutomated program verification is important as it has the potential to reduce the resources required by software development and improve the quality. Higher-order program verification is becoming increasingly important since the use of languages with higher-order features is rising and language versions such as Java 8 and C++11 have added support for higher-order functions.The project proposes to examine the expressive power of higher-order Horn clauses by comparing them to other formalisms of verification. Specifically, it will investigate how to express modal mu-calculus model checking problems as higher-order Horn clause problems, possibly by extending the syntax of higher-order Horn clauses to allow for the fact that modal mu-calculus allows both least and greatest fixpoint operators. This is expected to lead to algorithms for generating systems of higher-order Horn clauses from existing program verification problems.Higher-order Horn Clauses have been investigated for the purposes of logic programming, but only recently as a tool for program verification, so there is much about them not currently known, and this pursues an original direction of research. First-order Horn clauses have been used as an intermediate format in program verification between translation and solving. This enables solving techniques to be more easily extended to many programming languages and means that a particular translator can be used with existing and future solvers thanks to separation of concerns. It also allows intermediate transformation steps that both produce and consume Horn clauses.However, first-order Horn clauses suffer imprecision when used with higher-order programs since they require working with a first-order approximation to the program's behaviour. Higher-order Horn clauses are a promising area of research since it is possible to use them to express higher-order program verification problems without losing information about the higher-order nature of the programs.This project would reveal the advantages and limitations of higher-order Horn clauses relative to similar approaches, and could indicate whether they can be as effective in higher-order program verification as first order Horn clauses are for first-order programs. This will then inform and encourage further development of techniques for working with higher-order Horn clauses.

这个项目属于EPSRC验证和正确性研究领域的福尔斯。自动程序验证很重要，因为它有可能减少软件开发所需的资源，提高质量。高阶程序验证变得越来越重要，因为使用高阶功能的语言越来越多，Java 8和C++11等语言版本增加了对高阶函数的支持。该项目建议通过将高阶Horn子句与其他形式化验证进行比较，来检查高阶Horn子句的表达能力。具体来说，它将研究如何将模态μ演算模型检查问题表示为高阶Horn子句问题，可能是通过扩展高阶Horn子句的语法来考虑模态μ演算允许最小和最大不动点算子的事实。这预计将导致算法生成系统的高阶霍恩条款从现有的程序验证problems.Higher-order霍恩条款已被调查的逻辑编程的目的，但最近作为一种工具，程序验证，所以有很多关于他们目前不知道，这追求一个原始的研究方向。一阶Horn子句在程序验证中被用作翻译和求解之间的中间格式。这使得求解技术能够更容易地扩展到许多编程语言，并意味着由于关注点的分离，特定的翻译器可以与现有和未来的求解器一起使用。它还允许中间转换步骤，产生和消耗Horn子句。然而，一阶Horn子句在用于高阶程序时会受到不精确性的影响，因为它们需要对程序的行为进行一阶近似。高阶Horn子句是一个很有前途的研究领域，因为它可以用来表达高阶程序验证问题，而不会丢失程序的高阶性质的信息。本项目将揭示高阶Horn子句相对于类似方法的优点和局限性，并且可以指示它们在高阶程序验证中是否可以像用于一阶程序的一阶Horn子句那样有效。这将为高阶Horn子句的进一步发展提供信息和鼓励。