| 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: |
|
| 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: |
|
| Related Grants: |
|
| Panel History: |
| Panel Date | Panel Name | Outcome |
|
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: |
|