Research Perspectives - Tools for Visualisation of Portfolios
EPSRC logo

EPSRC Database


Source RCUK EPSRC Data

EP/H017585/1 - Verification of Shared-Memory Concurrent Software

Research Perspectives grant details from EPSRC portfolio

http://www.researchperspectives.org/gow.grants/grant_EPH0175851.png

Professor D Kroening EP/H017585/1 - Verification of Shared-Memory Concurrent Software

Principal Investigator - Computer Science, University of Oxford

Other Investigators

Professor J Ouaknine, Co InvestigatorProfessor J Ouaknine

Scheme

Standard Research

Research Areas

Verification and Correctness Verification and Correctness

Start Date

09/2010

End Date

02/2014

Value

£428,481

Similar Grants

Automatic generation of similar EPSRC grants

Similar Topics

Topic similar to the description of this grant

Grant Description

Summary and Description of the grant

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.

Structured Data / Microdata


Grant Event Details:
Name: Verification of Shared-Memory Concurrent Software - EP/H017585/1
Start Date: 2010-09-01T00:00:00+00:00
End Date: 2014-02-28T00:00:00+00:00

Organization: University of Oxford

Description: 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 o ...