Resource Reasoning

Lead Research Organisation: Queen Mary, University of London
Department Name: Computer Science

Abstract

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.

Publications

10 25 50
publication icon
Dinsdale-Young T (2018) A perspective on specifying and verifying concurrent modules in Journal of Logical and Algebraic Methods in Programming

Related Projects

Project Reference Relationship Related To Start End Award Value
EP/H008373/1 01/01/2010 01/03/2012 £3,189,258
EP/H008373/2 Transfer EP/H008373/1 01/03/2012 30/06/2016 £2,248,640
 
Description We discovered that logics of resources can be more useful for analyzing computer programs than previously thought. This includes breadth in treatment of various kinds of programs (web, object-oriented, imperative) and in the scale of the programs themselves. Very significant results we obtained for concurrent programs and for automatic program analysis.
Exploitation Route We hope that these findings will be helpful to scientists in developing better techniques for analyzing software, and to industry in applying such techniques.
Sectors Digital/Communication/Information Technologies (including Software)

 
Description This grant did some of the science which influenced the startup company Monoidics. In particular, the technique of bi-abduction was worked on in this project and published in a paper.
First Year Of Impact 2009
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Societal,Economic