EPSRC logo

Details of Grant 

EPSRC Reference: EP/H017585/1
Title: Verification of Shared-Memory Concurrent Software
Principal Investigator: Kroening, Professor D
Other Investigators:
Ouaknine, Professor J
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: University of Oxford
Scheme: Standard Research
Starts: 01 September 2010 Ends: 28 February 2014 Value (£): 428,481
EPSRC Research Topic Classifications:
Fundamentals of Computing Software Engineering
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
30 Sep 2009 ICT Prioritisation Panel (Oct 09) Announced
Summary on Grant Application Form
Software products are becoming increasingly complex. One of the chiefreasons for this is the demand for concurrent software thatefficiently exploits multiple execution cores. Such systems, such asIntel's Core Duo, have become ubiquitous over the last two or threeyears. Unfortunately, developing reliable concurrent programs is adifficult and specialised task, requiring highly skilled engineers,most of whose efforts are spent on the testing and validationphases. As a result, there is a strong economic andstrategic incentive for software houses to automate parts of theverification process.Random simulation and testing, while automated, has severelimitations, particularly in the case of concurrent software, in whichthe plethora of possible thread interleavings often conspires toconceal design flaws. Formal verification, on the other hand, can alsobe automated, and tools that implement it check a concurrent programfor all its possible behaviours.Numerous tools to hunt down functional flaws in hardware designs have beenavailable commercially for a number of years. The use of such tools iswidespread, and there is a broad range of vendors. In contrast, the marketfor formal tools that address the need for quality software---and even moreso for concurrent software---is still in its infancy.The proposed research project focuses on shared-variableconcurrency, i.e., eliminating programming errors related tomulti-threaded programs in which the threads communicate via a sharedportion of the memory. This programming paradigm is frequently used,and is the predominant form of concurrency on commodity computingsystems. Furthermore, errors relating to concurrency often depend onthe process schedule, which is difficult to control. As a consequence,such errors are difficult to test for and to reproduce, yet can havewide-ranging and potentially devastating consequences.We propose to investigate (i) verification by means of automatedsummarisation of threads, (ii) identification of transactions,enabling partial-order reductions, and (iii) Craiginterpolation to derive thread invariants. Our primary target arelow-level applications written in C/C++, and we will supportboth the POSIX thread API and the WIN32 thread API to maximizethe applicability of our research. We will evaluate the benefit of ourmethods and tools in collaboration with industrial users.
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
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
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: http://www.ox.ac.uk