EPSRC logo

Details of Grant 

EPSRC Reference: EP/K039431/1
Title: Partial order semantics for concurrent program verification
Principal Investigator: Alglave, Dr J
Other Investigators:
Researcher Co-Investigators:
Project Partners:
IBM Monoidics Ltd
Department: Computer Science
Organisation: UCL
Scheme: First Grant - Revised 2009
Starts: 26 February 2014 Ends: 25 February 2016 Value (£): 98,000
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
05 Jun 2013 EPSRC ICT Responsive Mode - Jun 2013 Announced
Summary on Grant Application Form
Multiprocessor machines are now predominant, as most laptops, desktops,

servers, mobile phones and aircrafts routinely have multiple to many cores.

Unfortunately, concurrent programming is error-prone, which now affects

everyone given this trend towards more and more concurrency.

Let us mention for example a recent concurrency bug found in the PostgreSQL

database (see

http://archives.postgresql.org/pgsql-hackers/2011-08/msg00330.php). PostgreSQL

is one of the most popular database nowadays, and many websites rely on its

correct functioning. This bug was particularly difficult to observe (and

indeed is not fixed yet) because it only occurred on a multicore machine, and a

particular hardware platform, IBM Power.

Reproducing such bugs is as hard as observing them; thus testing can hardly

discover them. To prove a program free of errors, we would like to devise

automated techniques that analyse the code without executing it. Thus,

we can relieve programmers from the burden of writing the proofs of their

programs.

Yet, automatic verification of concurrent programs represents a challenge,

whether it aims at proving the full correctness of a program (e.g. a

program sorting a list actually sorts the list), or at checking specific

properties (e.g. the program is free of data races) short of full

correctness. We focus here on the latter: we would like to enhance

the scalability of tools checking that a concurrent program does not violate

certain safety-critical properties of interest.

We would like to show that scalable automatic verification can be achieved by

exploiting the rich history of partial orders for modeling concurrency.

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: