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
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
(2016)
Abstraction refinement guided by a learnt probabilistic model
in ACM SIGPLAN Notices
Oh H
(2015)
Selective X-Sensitive Analysis Guided by Impact Pre-Analysis
in ACM Transactions on Programming Languages and Systems
Peleg H
(2015)
Symbolic automata for representing big code
in Acta Informatica
Kanovich M
(2012)
Light linear logics with controlled weakening: Expressibility, confluent strong normalization
in Annals of Pure and Applied Logic
Albarghouthi Aws
(2015)
Spatial Interpolants
in arXiv e-prints
Gardner P
(2014)
Abstract Local Reasoning for Concurrent Libraries: Mind the Gap
in Electronic Notes in Theoretical Computer Science
Lozes É
(2012)
Shared Contract-Obedient Endpoints
in Electronic Proceedings in Theoretical Computer Science
Brookes S
(2014)
The Essence of Reynolds
in Formal Aspects of Computing
Lee O
(2012)
A divide-and-conquer approach for analysing overlaid data structures
in Formal Methods in System Design
Kanovich M
(2014)
Bounded memory Dolev-Yao adversaries in collaborative systems
in Information and Computation
GOTSMAN A
(2013)
Modular verification of preemptive OS kernels
in Journal of Functional Programming
Pym D
(2012)
A proof-theoretic analysis of the classical propositional matrix method
in Journal of Logic and Computation
Pym D
(2017)
A Substructural Modal Logic of Utility
in Journal of Logic and Computation
Collinson M
(2014)
A substructural logic for layered graphs
in Journal of Logic and Computation
Collinson M
(2017)
Layered graph logic as an assertion language for access control policy models
in Journal of Logic and Computation
Dahlqvist F
(2017)
Coalgebraic completeness-via-canonicity for distributive substructural logics
in Journal of Logical and Algebraic Methods in Programming
O'Hearn P
(2015)
On the relation between Concurrent Separation Logic and Concurrent Kleene Algebra
in Journal of Logical and Algebraic Methods in Programming
Brotherston J
(2014)
Undecidability of Propositional Separation Logic and Its Neighbours
in Journal of the ACM
Gotsman A
(2013)
Linearizability with Ownership Transfer
in Logical Methods in Computer Science
Thamsborg J
(2012)
Two for the Price of One: Lifting Separation Logic Assertions
in Logical Methods in Computer Science
Brotherston, James
(2014)
Cyclic Abduction of Inductively Defined Safety and Termination Preconditions
in Proceedings of SAS-21
Cook, B
(2014)
Disproving Termination with Overapproximation
in Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD '14)
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)
Lozes É
(2015)
Shared contract-obedient channels
in Science of Computer Programming
Brotherston J
(2012)
Bunched Logics Displayed
in Studia Logica
Anderson G
(2016)
A calculus and logic of bunched resources and processes
in Theoretical Computer Science
Courtault J
(2016)
A logic of separating modalities
in Theoretical Computer Science
Cook B
(2015)
Embracing Overapproximation for Proving Nontermination
in Tiny Transactions on Computer Science,
Da Rocha Pinto P
(2014)
ECOOP 2014 - Object-Oriented Programming
Gardner P
(2014)
Programming Languages and Systems
Burckhardt S
(2014)
Replicated data types
Grigore R
(2016)
Abstraction refinement guided by a learnt probabilistic model
Anderson G
(2016)
Decision and Game Theory for Security
Grigore R
(2015)
Abstraction Refinement Guided by a Learnt Probabilistic Model
Brotherston J
(2016)
Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
Brockschmidt M,
(2016)
T2: temporal property verification
Hobor A
(2013)
The ramifications of sharing in data structures
Peleg H
(2013)
Static Analysis
Naik M
(2012)
Abstractions from tests
Brotherston, J
(2016)
Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
Van De Meent JW
(2015)
Particle Gibbs with Ancestor Sampling for Probabilistic Programs
Zhang X
(2014)
Hybrid top-down and bottom-up interprocedural analysis
Burckhardt S
(2012)
Programming Languages and Systems
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. |