EPSRC logo

Details of Grant 

EPSRC Reference: EP/K009907/1
Title: Verification of Concurrent and Higher-Order Recursive Programs
Principal Investigator: Hague, Dr M
Other Investigators:
Researcher Co-Investigators:
Project Partners:
University of Edinburgh University of Paris East Marne La Vallee
Department: Computer Science
Organisation: Royal Holloway, Univ of London
Scheme: EPSRC Fellowship
Starts: 01 May 2013 Ends: 30 April 2018 Value (£): 469,677
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
16 Jan 2013 EPSRC ICT Responsive Mode - Jan 2013 Deferred
21 Feb 2013 ICT Fellowships Interview Meeting - Feb 2013 Announced
Summary on Grant Application Form
Global society increasingly relies on devices controlled by software, from TV

sets to vehicle braking systems. It is considered a "fact-of-life" that

software contains errors, which can come at great cost, such as the Mars Polar

Lander crash or the 1992 failure of the London Ambulance Dispatch Service. In a

2008 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 situations

as possible. However, it is not feasible to run a program under all

environments. Hence, testing relies on the perspicacity of the testing engineer

who must carefully choose environments that may expose flaws.

Modern computers increase performance by allowing many computer programs to run

concurrently. Anticipating the interactions of even as a little as two programs

is an extremely difficult task, and errors are often difficult to replicate and

diagnose. Furthermore, the efficiency of hardware is often increased by

permitting 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 a

program behaves as expected under all conditions. This area has flourished

recently, including a 2007 Turing Award for Clarke, Emerson and Sifakis, who

transformed the technique from a theoretical pursuit into an industrially

applicable product. Model-checking is embraced by companies like Microsoft (to

improve its Windows OS) and Altran-Praxis (for safety-critical software).

However, model-checkers must rely on simplified models of computer programs to

guarantee results, leading to many correct programs being labelled erroneous.

This is a design choice, following the argument that it it better to raise a

false alarm, than let an error pass by.

However, a large number of false alarms damage reliability and usability --- a

software 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 scale

deployment of such tools. The goal of this fellowship is to increase the

precision of verification tools --- reducing the number of false alarms ---

while retaining the efficiency of current techniques, resulting in

model-checking tools that are more reliable and usable.

During this fellowship, we will construct a state-of-the-art verification

framework, unifying several prototypical tools and requiring novel

model-checking techniques, and permitting new ideas to be experimented with

quickly. The framework will be tested on real-world software to ensure its

usability and reliability. It will accurately model difficult programming

paradigms, 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 bring

together researchers at Oxford University, Universite Paris-Est, and Universite

Paris-Diderot as well as the CARP project, based across several universities and

companies world-wide, and researchers at Microsoft Research, Cambridge.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: