Resource Reasoning
Lead Research Organisation:
University College 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
Albarghouthi Aws
(2015)
Spatial Interpolants
in arXiv e-prints
Anand S
(2012)
Automated concolic testing of smartphone apps
Anderson G
(2016)
A calculus and logic of bunched resources and processes
in Theoretical Computer Science
Anderson G
(2016)
Decision and Game Theory for Security
Brockschmidt M
(2014)
Tools and Algorithms for the Construction and Analysis of Systems
Brockschmidt M
(2013)
Computer Aided Verification
Brockschmidt M,
(2016)
T2: temporal property verification
Brookes S
(2014)
The Essence of Reynolds
in Formal Aspects of Computing
Brotherston J
(2012)
Programming Languages and Systems
Brotherston J
(2012)
Bunched Logics Displayed
in Studia Logica
Description | This project has been about local reasoning about resources. It arose from work on various forms of separation logic and its associated automatic verification tools for computer programs. The ongoing project is to develop an elegant theory (or theories) of resource reasoning that meshes with programmers' informal intuitions and leads to tractable analysis and verification techniques for a range of problem domains, such as classic operating systems, the evolving world of web software, and concurrent programming. |
Exploitation Route | The ideas developed in this project are contributing to new project proposals in areas diverse as distributed systems and reasoning about security policies in human-centred organizations. Several members of the project (or people associated with the project) are now working with major companies, including Amazon, Facebook, and Google, where ideas from this project are directly impacting upon major R&D projects. |
Sectors | Digital/Communication/Information Technologies (including Software) |
URL | http://www.resourcereasoning.com |
Description | The results of the Resource Reasoning project have had significant influence on program analysis and verification operations in Facebook and Amazon, through the Infer program analysis tool. The Infer tool has now been made open source by Facebook: https://engineering.fb.com/2015/06/11/developer-tools/open-sourcing-facebook-infer-identify-bugs-before-you-ship/. The Infer tool is now used by a very wide range of organizations; see https://fbinfer.com > Who Uses Infer. Many of the people involved with Resource Reasoning have gone on to have substantive careers in high-tech industry and academia, including leadership roles in global corporations. The range of activities in the project that were based on, and which developed, Separation Logic has led to Separation Logic, its variants, and its applications being a major topic of research in leading conferences such as Principles of Programming Languages (PoPL) and others. The results of the project had some formative influence on the 'Interface Reasoning for Interacting Systems (IRIS)' programme grant funded by EPSRC, which is tackling foundational problems about modelling and reasoning about complex composite systems at all scales from code through to organization structure. |
First Year Of Impact | 2015 |
Sector | Digital/Communication/Information Technologies (including Software),Security and Diplomacy |
Impact Types | Societal Economic Policy & public services |
Description | Facebook Faculty Grant to James Brotherston 2015 |
Amount | $30,000 (USD) |
Organisation | |
Sector | Private |
Country | United States |
Start | 09/2015 |
End | 09/2018 |
Title | CYCLIST |
Description | : Generic cyclic theorem prover, instantiation to symbolic-heap separation logic plus associated tools for same |
Type Of Material | Improvements to research infrastructure |
Year Produced | 2014 |
Provided To Others? | Yes |
Impact | Regularly cited in the academic literature on theorem proving and separation logic. |
URL | https://github.com/ngorogiannis/cyclist |
Title | julia systems modelling package |
Description | Packages for the julia (www.julialang.org) modelling languages that capture our systems and security modelling approach. Presentation in progress. |
Type Of Material | Improvements to research infrastructure |
Year Produced | 2016 |
Provided To Others? | Yes |
Impact | Presentations at the UK Research Institute in the Science of Cybersecurity (RISCS) first-phase final meeting. http://www.riscs.org.uk/?page_id=15 |
URL | https://github.com/tristanc/SysModels |
Description | Collaboration with INRIA and Université de Lorraine |
Organisation | The National Institute for Research in Computer Science and Control (INRIA) |
Country | France |
Sector | Public |
PI Contribution | Research collaboration in theory of substructural modal logics and their application in systems and security modelling. |
Collaborator Contribution | Research collaboration in theory of substructural modal logics and their application in systems and security modelling. |
Impact | J.-R. Courtault, D. Galmiche, and D. Pym. A Logic of Separating Modalities. Accepted for publication in Theoretical Computer science, subject to minor revisions. Further research and publications are ongoing. |