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)
Decision and Game Theory for Security
Anderson G
(2016)
A calculus and logic of bunched resources and processes
in Theoretical Computer Science
Brockschmidt M
(2013)
Computer Aided Verification
Brockschmidt M
(2014)
Tools and Algorithms for the Construction and Analysis of Systems
Brockschmidt M,
(2016)
T2: temporal property verification
Brookes S
(2014)
The Essence of Reynolds
in Formal Aspects of Computing
Brotherston J
(2014)
Cyclic Abduction of Inductively Define Safety and Termination Preconditions
Brotherston J
(2012)
Programming Languages and Systems
Brotherston J
(2016)
Sub-Classical Boolean Bunched Logics and the Meaning of Par
Brotherston J
(2012)
Bunched Logics Displayed
in Studia Logica
Brotherston J
(2014)
Parametric completeness for separation theories
Brotherston J
(2016)
Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
Brotherston J
(2014)
Undecidability of Propositional Separation Logic and Its Neighbours
in Journal of the ACM
Brotherston, J
(2016)
Model Checking for Symbolic-Heap Separation Logic with Inductive Predicates
Brotherston, James
(2014)
Cyclic Abduction of Inductively Defined Safety and Termination Preconditions
in Proceedings of SAS-21
Burckhardt S
(2012)
Programming Languages and Systems
Burckhardt S
(2014)
Replicated data types
Collinson M
(2017)
Layered graph logic as an assertion language for access control policy models
in Journal of Logic and Computation
Collinson M
(2014)
A substructural logic for layered graphs
in Journal of Logic and Computation
Cook B
(2014)
Disproving termination with overapproximation
Cook B
(2015)
Embracing Overapproximation for Proving Nontermination
in Tiny Transactions on Computer Science,
Cook, B
(2014)
Disproving Termination with Overapproximation
in Proceedings of the 14th International Conference on Formal Methods in Computer-Aided Design (FMCAD '14)
Courtault J
(2016)
A logic of separating modalities
in Theoretical Computer Science
Da Rocha Pinto P
(2014)
ECOOP 2014 - Object-Oriented Programming
Dahlqvist F
(2017)
Coalgebraic completeness-via-canonicity for distributive substructural logics
in Journal of Logical and Algebraic Methods in Programming
Dahlqvist F
(2015)
Relational and Algebraic Methods in Computer Science
Dinsdale-Young T
(2013)
Views
Docherty S
(2016)
Automated Reasoning
Gardner P
(2014)
Programming Languages and Systems
Gardner P
(2012)
Towards a program logic for JavaScript
Gardner P
(2014)
Abstract Local Reasoning for Concurrent Libraries: Mind the Gap
in Electronic Notes in Theoretical Computer Science
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)
Gotsman A
(2012)
Distributed Computing
GOTSMAN A
(2013)
Modular verification of preemptive OS kernels
in Journal of Functional Programming
Gotsman A
(2013)
Linearizability with Ownership Transfer
in Logical Methods in Computer Science
Grigore R
(2016)
Abstraction refinement guided by a learnt probabilistic model
Hoare T
(2014)
Relational and Algebraic Methods in Computer Science
Hobor A
(2013)
The ramifications of sharing in data structures
Kanovich M
(2014)
Bounded memory Dolev-Yao adversaries in collaborative systems
in Information and Computation
| 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. |