Expressivity and Algorithmics of Higher-Order Horn Clauses

本项目属于EPSRC验证和正确性研究领域自动化程序验证非常重要，因为它有可能减少软件开发所需的资源并提高质量。高阶程序验证随着高阶特征语言的使用而变得越来越重要，Java 8和C++11等语言版本也增加了对高阶函数的支持，该项目提出通过将高阶Horn子句与其他验证形式进行比较来检验它们的表达能力。具体地说，它将研究如何将情态u演算模型检验问题表示为高阶Horn子句问题，可能是通过扩展高阶Horn子句的语法来允许情态u演算允许最小和最大不动点算子的事实。高阶Horn子句的研究是为了逻辑编程的目的，但作为程序验证的工具是最近才开始的，因此目前还有很多关于高阶Horn子句的未知之处，这是一个原创性的研究方向。一阶Horn子句在程序验证中被用作翻译和求解之间的中间格式。这使得求解技术可以更容易地扩展到许多编程语言，并意味着由于关注点分离，特定的翻译器可以与现有和未来的解算器一起使用。它还允许产生和使用Horn子句的中间转换步骤。然而，当与高阶程序一起使用时，一阶Horn子句受到不精确的影响，因为它们需要与程序行为的一阶近似一起工作。高阶Horn子句是一个很有前途的研究领域，因为它可以用来表示高阶程序验证问题，而不会丢失关于程序的高阶性质的信息。该项目将揭示高阶Horn子句相对于类似方法的优势和局限性，并表明它们在高阶程序验证中是否能够像一阶Horn子句那样有效。这将通知并鼓励进一步开发使用高阶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.