Verification of Concurrent and Higher-Order Recursive Programs

从电视机到汽车制动系统，全球社会越来越依赖软件控制的设备。软件包含错误被认为是一个“生活事实”，这可能会带来巨大的代价，比如火星极地登陆器坠毁或1992年伦敦救护车调度服务的失败。在2008年的一项研究中，美国国家标准与技术研究院（NIST）估计，有缺陷的软件每年给美国经济造成595亿美元的损失。传统的软件测试是通过在尽可能多的困难情况下运行它。然而，在所有环境下运行程序是不可行的。因此，测试依赖于测试工程师的洞察力，他们必须仔细选择可能暴露缺陷的环境。现代计算机通过允许许多计算机程序并行运行来提高性能。预测两个程序之间的相互作用是一项极其困难的任务，而且错误通常很难复制和诊断。此外，硬件的效率通常通过允许软件开发人员意想不到的行为而提高。另一种确保正确性的方法是模型检查。模型检查尝试使用全自动技术来证明程序在所有条件下的行为都符合预期。这一领域最近蓬勃发展，Clarke、Emerson和Sifakis获得了2007年图灵奖，他们将这项技术从理论追求转化为工业应用产品。模型检查被微软（用于改进其Windows操作系统）和Altran-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.