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

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

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.