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
Schwinghammer J
(2011)
Nested Hoare Triples and Frame Rules for Higher-order Store
Schwinghammer J
(2011)
Nested Hoare Triples and Frame Rules for Higher-order Store
in Logical Methods in Computer Science
Da Rocha Pinto P
(2015)
Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)
in Electronic Notes in Theoretical Computer Science
Ntzik G
(2015)
Reasoning about the POSIX file system: local update and global pathnames
in ACM SIGPLAN Notices
Raad A
(2016)
Programming Languages and Systems
Raad A
(2016)
Programming Languages and Systems
Ntzik G.
(2018)
A concurrent specification of POSIX file systems
in Leibniz International Proceedings in Informatics, LIPIcs
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 |