EPSRC logo

Details of Grant 

EPSRC Reference: EP/H008373/1
Title: Resource Reasoning
Principal Investigator: OHearn, Professor P
Other Investigators:
Cook, Professor B YANG, Dr H Calcagno, Dr C
Gardner, Professor P
Researcher Co-investigators:
Project Partners:
Department: Computer Science
Organisation: Queen Mary, University of London
Scheme: Programme Grants
Starts: 01 January 2010 Ends: 01 March 2012 Value (£): 3,189,258
EPSRC Research Topic Classifications:
Computer Sys. & Architecture Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
15 Jul 2009 ICT Programme Grants (July 09) Announced
Summary on Grant Application Form
Resource has always been a central concern in computer systems. In classical operating systems for example, processes access system resources such as memory, locks, files, processor time, and network bandwidth; correct resource usage is essential for the overall working of the system. In the World Wide Web, the whole structure can be regarded as a giant, dynamic resource net, with its Uniform ResourceIdentifiers referring to located data and code. Generally, for all kinds of computer system, it is second nature for a programmer to think carefully about the way the system handles resource as part of the programming task in hand. The point of view of this research is that there can be a novel kind of mathematical theory, which we call resource reasoning, which goes hand in hand with programmers' informal thinking about resources. The first stage of such a theory is represented by Separation Logic and its relatives, developments which are suggestive of much more. Our hypothesis is that, just as `resource-oriented thinking' occupies a central position in pre-formal system design, resource is also central to the formal analysis and verification of programs across the modern-day and future computing infrastructure. The challenge is to develop an elegant theory (or theories) of resource reasoning, that both meshes with programmers' and system designers' informal intuitions, and leads to tractable analysis and verification techniques for a range of problem domains such as classic operating systems, the continually-evolving web software, concurrent programming, and even hardware synthesis.The project will provide new theoretical concepts and new prototype tools that will eventually help to make computers that crash less frequently, mishandle our data less frequently, and generally have improved reliability.
Key Findings
No information has been submitted for this grant.
Potential use in non-academic contexts
No information has been submitted for this grant.
No information has been submitted for this grant.
Sectors submitted by the Researcher
No information has been submitted for this grant.
Project URL:  
Further Information:  
Organisation Website: http://www.qmul.ac.uk