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
Lee O
(2012)
A divide-and-conquer approach for analysing overlaid data structures
in Formal Methods in System Design
Pym D
(2012)
A proof-theoretic analysis of the classical propositional matrix method
in Journal of Logic and Computation
Kanovich M
(2012)
Light linear logics with controlled weakening: Expressibility, confluent strong normalization
in Annals of Pure and Applied Logic
Giesl, J
(2012)
Symbolic Evaluation Graphs and Term Rewriting: A General Methodology for Analyzing Logic Programs
in Proceedings of the 14th International Symposium on Principles and Practice of Declarative Programming (PPDP '12)
Naik M
(2012)
Abstractions from tests
Brotherston J
(2012)
Bunched Logics Displayed
in Studia Logica
Burckhardt S
(2012)
Programming Languages and Systems
Gardner P
(2012)
Towards a program logic for JavaScript
Thamsborg J
(2012)
Two for the Price of One: Lifting Separation Logic Assertions
in Logical Methods in Computer Science
Brotherston J
(2012)
Programming Languages and Systems
Gotsman A
(2012)
Distributed Computing
Anand S
(2012)
Automated concolic testing of smartphone apps
Lozes É
(2012)
Shared Contract-Obedient Endpoints
in Electronic Proceedings in Theoretical Computer Science
Gotsman A
(2013)
Linearizability with Ownership Transfer
in Logical Methods in Computer Science
GOTSMAN A
(2013)
Modular verification of preemptive OS kernels
in Journal of Functional Programming
Peleg H
(2013)
Static Analysis
Hobor A
(2013)
The ramifications of sharing in data structures
Brockschmidt M
(2013)
Computer Aided Verification
Dinsdale-Young T
(2013)
Views
Da Rocha Pinto P
(2014)
ECOOP 2014 - Object-Oriented Programming
Gardner P
(2014)
Programming Languages and Systems
Burckhardt S
(2014)
Replicated data types
Collinson M
(2014)
A substructural logic for layered graphs
in Journal of Logic and Computation
Zhang X
(2014)
Hybrid top-down and bottom-up interprocedural analysis
Cook, B
(2014)
Disproving Termination with Overapproximation
in Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD '14)
Brotherston J
(2014)
Undecidability of Propositional Separation Logic and Its Neighbours
in Journal of the ACM
Brotherston J
(2014)
Cyclic Abduction of Inductively Define Safety and Termination Preconditions
Hoare T
(2014)
Relational and Algebraic Methods in Computer Science
Brotherston J
(2014)
Parametric completeness for separation theories
Brotherston, James
(2014)
Cyclic Abduction of Inductively Defined Safety and Termination Preconditions
in Proceedings of SAS-21
Gardner P
(2014)
Abstract Local Reasoning for Concurrent Libraries: Mind the Gap
in Electronic Notes in Theoretical Computer Science
Cook B
(2014)
Disproving termination with overapproximation
O'Hearn P.W.
(2014)
The Essence of Reynolds
Zhang X
(2014)
On abstraction refinement for program analyses in Datalog
Brockschmidt M
(2014)
Tools and Algorithms for the Construction and Analysis of Systems
Brookes S
(2014)
The Essence of Reynolds
in Formal Aspects of Computing
Kanovich M
(2014)
Bounded memory Dolev-Yao adversaries in collaborative systems
in Information and Computation
Mangal R
(2014)
Programming Languages and Systems
Kanovich, M
(2014)
Foundations for Decision Problems in Separation Logic with General Inductive Predicates
in 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)
Grigore R
(2015)
Abstraction Refinement Guided by a Learnt Probabilistic Model
Albarghouthi Aws
(2015)
Spatial Interpolants
in arXiv e-prints
Van De Meent JW
(2015)
Particle Gibbs with Ancestor Sampling for Probabilistic Programs
O'Hearn P.W.
(2015)
Moving Fast with Software Verification
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 | 10/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. |