Compositional Higher-Order Model Checking: Logics, Models and Algorithms

无缺陷程序的构建是一个具有国际重要性和巨大潜在影响的具有挑战性的研究问题。然而，传统的方法来实现软件的信心，如测试和调试，是不有效的，往往占总开发成本的50-75%。在过去的十年中，自动验证技术，如模型检查，已经取得了很大的进展，以弥补这种情况，特别是当应用于一阶命令式程序，如C。模型检查是一种程序验证方法，它保证了下推自动化的准确分析。为了根据正确性属性对程序进行模型检查，首先将正确性属性表示为可判定逻辑的公式。然后，一个抽象的，通常是有限的，系统的模型被构造，然后被彻底检查违反公式。SLAM和Terminator等工具证明了模型检查对于类C程序具有可扩展性且高效。该项目是关于模型检查及其相关自动验证方法在高阶函数式程序中的应用。函数式程序长期以来一直被应用于现实世界的任务。程序员使用函数式语言是因为他们可以更快地构建更健壮的代码，并且错误更少，从而提高了可靠性并降低了成本。其他人转向函数式语言，因为它们在数据并行性，并发性，GPGPU和云编程方面提供了优势。示例：Microsoft .NET语言F#已成为金融和科学应用程序中的首选原型语言。面向并发的函数式语言Erlang非常适合编程多核CPU、网络服务器、分布式数据库、GUI以及监视、控制和测试工具。因此，通过使函数式编程更安全，更强大和更高效，用于函数式程序正式分析的技术和工具支持将为整个数字经济带来重大利益，特别是金融建模，科学应用，计算和电信，这对当前和未来的英国经济成功至关重要。我们的目标是开发一个可扩展的，一个全自动和良好的方法验证功能程序，基于组合方法高阶模型检查。我们的方法很新颖：我们将语义方法（特别是游戏语义和交集类型）与来自自动验证和程序分析的算法和自动机理论技术相结合。验证问题本质上是具有挑战性的，尤其是因为其超指数最坏情况的复杂性。尽管如此，我们的模型检测算法，PREFACE的原型实现，很容易扩展到递归方案的数千条规则，远远超出了目前最先进的高阶模型检查器的能力，从而表明我们的方法是非常有前途的。因此，我们的研究假设：这是可能的设计良好的基础，但实际的程序验证程序。这将通过基于组合高阶模型检查的原则性方法来实现。

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. In the past decade, automated verification techniques such as model checking have made great strides towards remedying this situation, especially when applied to first-order imperative programs such as C. Model checking is an approach to program verification that promises accurate analysis with pushdown automation. To model check a program against a correctness property, one first expresses the correctness property as a formula of a decidable logic. Then an abstract, typically finite, model of the system is constructed, which is then checked exhaustively for violation of the formula. Tools such as SLAM and Terminator demonstrate that model checking is scalable and highly effective for C-like programs.This project is about the application of model checking and its allied automated verification methods to 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 then 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. Examples: The Microsoft .NET language F# has emerged as a prototyping language of choice in finance and scientific applications. The concurrency-oriented functional language Erlang is a natural fit for programming multicore CPUs, networked servers, distributed databases, GUIs, and monitoring, control and testing tools. 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.Our GOAL is to develop a scalable, fully-automatic and well-founded method for the verification of functional programs, based on a compositional approach to Higher-Order Model Checking. Our approach is novel: we marry semantic methods (notably game semantics and intersection types) with algorithmic and automata-theoretic techniques from automated verification and program analysis. The verification problem is intrinsically challenging, not least because of its hyper-exponential worst-case complexity. Nevertheless a prototype implementation of our model checking algorithm, PREFACE, readily scales to recursion schemes of thousands of rules, well beyond the capabilities of current state-of-the-art higher-order model checkers, thus indicating that our approach is very promising. Hence our RESEARCH HYPOTHESIS: It is possible to design well-founded yet practical program verification procedures. This will be achieved by a principled approach based on COMPOSITIONAL Higher-Order Model Checking.