Programmers already think about resources like memory and network bandwidth when they write code, but the mathematical tools to formally verify that code handles those resources correctly have lagged behind. This project aims to close that gap by developing a new mathematical theory—called resource reasoning—that formalises the informal, intuitive ways programmers already manage resources in systems ranging from operating systems to the web. The core hypothesis is that resource thinking is not just a practical habit but a fundamental principle that can underpin rigorous program verification. If successful, the research would produce both theoretical concepts and prototype tools that make it possible to prove, mathematically, that software handles resources correctly. The practical payoff would be computers that crash less often, mishandle data less frequently, and generally behave more reliably—without requiring programmers to change how they think. This is primarily fundamental science: building a mathematical foundation for reasoning about resources, analogous to how Separation Logic provided a foundation for reasoning about memory. The work targets the computing infrastructure that quietly underpins everything from operating systems to web services, but it does not promise a specific consumer product or near-term fix.
View original technical description
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.
Plain English summaries and category classifications on this site are generated by AI and may not perfectly reflect the original research.
Is something wrong? Let us know