Verification of Concurrent and Higher-Order Recursive Programs

全球社会越来越依赖于由软件控制的设备，从电视机到汽车制动系统。软件包含错误被认为是“生活中的事实”，这可能会带来巨大的代价，例如火星极地着陆器坠毁或1992年伦敦救护车调度服务的失败。在2008年的一项研究中，美国NIST机构估计，有缺陷的软件每年给美国经济造成595亿美元的损失。然而，要在所有环境下运行一个程序是不可行的.因此，测试依赖于测试工程师的洞察力，他们必须仔细选择可能暴露缺陷的环境。现代计算机通过允许许多计算机程序并发运行来提高性能。预测哪怕是两个程序之间的交互也是一项极其困难的任务，而且错误通常很难复制和诊断。此外，硬件的效率通常通过允许软件开发人员不期望的行为来提高。另一种确保正确性的方法是模型检查，模型检查试图使用全自动的技术来证明程序在所有条件下的行为都符合预期。这一领域最近取得了长足的进步，包括2007年Clarke、Emerson和Sifakis的图灵奖，他们将这项技术从理论上的追求转化为工业上可应用的产品。模型检查被微软（用于改进其Windows操作系统）和Altrans-Praxis（用于安全关键软件）等公司所采用。然而，模型检查器必须依赖于计算机程序的简化模型来保证结果，导致许多正确的程序被贴上错误的标签。这是一种设计选择，遵循的论点是，发出错误警报比让错误通过更好。然而，大量的错误警报会损害可靠性和可用性-如果大多数错误实际上根本不是错误，软件开发人员就不会仔细研究报告的错误。这是大规模部署此类工具时的一个真实的问题。该奖学金的目标是提高验证工具的精度-减少错误警报的数量-同时保持当前技术的效率，从而使模型检查工具更加可靠和可用。在这个奖学金期间，我们将构建一个最先进的验证框架，统一几个原型工具，需要新颖的模型检查技术，并允许新的想法被迅速实验。该框架将在真实世界的软件上进行测试，以确保其可用性和可靠性。它将准确地模拟困难的编程范例，如现代并发行为和“高阶”结构这项研究将在伦敦帝国理工学院进行，并将汇集牛津大学，巴黎东部大学和巴黎狄德罗大学的研究人员以及CARP项目，该项目位于世界各地的几所大学和公司，和研究人员在微软研究院，剑桥。

Global society increasingly relies on devices controlled by software, from TVsets to vehicle braking systems. It is considered a "fact-of-life" thatsoftware contains errors, which can come at great cost, such as the Mars PolarLander crash or the 1992 failure of the London Ambulance Dispatch Service. In a2008 study, the US NIST agency estimates faulty software costs the US economy$59.5bn annually.Classically software is tested by running it under as many difficult situationsas possible. However, it is not feasible to run a program under allenvironments. Hence, testing relies on the perspicacity of the testing engineerwho must carefully choose environments that may expose flaws. Modern computers increase performance by allowing many computer programs to runconcurrently. Anticipating the interactions of even as a little as two programsis an extremely difficult task, and errors are often difficult to replicate anddiagnose. Furthermore, the efficiency of hardware is often increased bypermitting behaviours a software developer would not expect. An alternative approach to ensuring correctness is model-checking.Model-checking attempts to use fully automatic techniques to prove that aprogram behaves as expected under all conditions. This area has flourishedrecently, including a 2007 Turing Award for Clarke, Emerson and Sifakis, whotransformed the technique from a theoretical pursuit into an industriallyapplicable product. Model-checking is embraced by companies like Microsoft (toimprove its Windows OS) and Altran-Praxis (for safety-critical software). However, model-checkers must rely on simplified models of computer programs toguarantee results, leading to many correct programs being labelled erroneous.This is a design choice, following the argument that it it better to raise afalse alarm, than let an error pass by. However, a large number of false alarms damage reliability and usability --- asoftware developer will not study reported errors carefully if the majority are,in fact, not errors at all. This is a real problem in the large scaledeployment of such tools. The goal of this fellowship is to increase theprecision of verification tools --- reducing the number of false alarms ---while retaining the efficiency of current techniques, resulting inmodel-checking tools that are more reliable and usable. During this fellowship, we will construct a state-of-the-art verificationframework, unifying several prototypical tools and requiring novelmodel-checking techniques, and permitting new ideas to be experimented withquickly. The framework will be tested on real-world software to ensure itsusability and reliability. It will accurately model difficult programmingparadigms, such as modern concurrent behaviours and "higher-order" constructs(increasingly embraced by state-of-the-art programming languages).The research will be carried out at Imperial College London, and will bringtogether researchers at Oxford University, Universite Paris-Est, and UniversiteParis-Diderot as well as the CARP project, based across several universities andcompanies world-wide, and researchers at Microsoft Research, Cambridge.