Verification of Concurrent and Higher-Order Recursive Programs

点击翻译按钮获取中文摘要

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.