EPSRC logo

Details of Grant 

EPSRC Reference: EP/K008528/1
Title: REMS: Rigorous Engineering for Mainstream Systems
Principal Investigator: Sewell, Professor PM
Other Investigators:
Pitts, Professor AM Gordon, Professor M Moore, Professor S
Crowcroft, Professor J Gardner, Professor P Stark, Dr I
Hand, Dr S
Researcher Co-Investigators:
Project Partners:
ARM Ltd IBM UK Ltd INRIA Paris - Rocquencourt
Microsoft PRECISE Center, University of Pennsylvan Purdue University
The FreeBSD Foundation University of Texas at Austin
Department: Computer Science and Technology
Organisation: University of Cambridge
Scheme: Programme Grants
Starts: 01 March 2013 Ends: 28 February 2020 Value (£): 5,575,635
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:
Panel DatePanel NameOutcome
22 Nov 2012 Programme Grant Interviews - 22 & 23 November 2012 (ICT) Announced
Summary on Grant Application Form
Computer systems are critical to modern society, from embedded devices and mobile phones through to internet services, but traditional computer engineering cannot produce reliable and secure systems, as we see in the continual stream of errors and security flaws impacting industry and consumers everywhere. Industry relies on informal prose specifications and ad hoc testing, but the complexity and scale of today's systems make it effectively impossible to exclude errors using only these methods (even though perhaps 70\% of development staff in major vendors are devoted to testing) and adversarial exploits all too often turn errors into major security concerns, with huge financial and social costs. Compounding the problem, the industry-wide abstractions around which real systems are built, including the architectural interfaces between multiprocessor hardware and software, and programming languages such as C and C++, are ill-defined, giving rise to ambiguity and error.

This is a long-standing problem, motivating extensive research on mathematically rigorous alternatives. Until now, it has been impractical to address mainstream widely-deployed systems with rigorous techniques. Academic research has focussed instead on modest-scale safety critical systems and academic verifications of idealised systems. There has been a deep disconnect between practical industrial engineering and systems research on the one hand, and theoretical research in semantics, verification, and foundations on the other. Now, however, the new approaches that we have, with a pragmatic emphasis on the use of mathematically rigorous models where they can be most effective, finally make it feasible to address industrial-scale systems--- and the commercial and social cost of not doing so is becoming ever greater. It is time for rigorous engineering of mainstream systems, unifying practice and theory.

REMS brings together a team of leading theory and systems researchers, with key industrial partners, to establish a new synthesis. We will establish a true engineering mathematics for the construction of more robust and secure computer systems: mathematically rigorous models, verification techniques, and engineering tools applied to the construction of full-scale mainstream computer systems, including key infrastructure in widespread use today (multiprocessors, programming languages, and operating systems). We will couple this with novel programming-language and verification support for future system-building. Developing our recent work with processor vendors and language standards bodies, we will address the technical, engineering and social challenges necessary to bring these techniques into widespread use, enabling a radical improvement in computer engineering as a whole.

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: http://www.cam.ac.uk