Every time a computer crashes or a web service fails, the root cause is often a programmer’s mistake in how the system handles resources like memory, files, or network bandwidth. This project aims to build a new mathematical theory—called resource reasoning—that formalises the informal, intuitive thinking programmers already do when managing resources. The first step in this direction, Separation Logic, has already shown promise, but the goal here is to develop a general, elegant theory that works across operating systems, web software, concurrent programs, and even hardware design. If successful, the research would produce both new theoretical concepts and prototype tools that can automatically verify whether a program handles resources correctly. That means fewer crashes, fewer data mishandling incidents, and more reliable software overall. This is fundamental, curiosity-driven work in computer science—not a product ready for market. But past work in this vein has already transformed how critical systems are built, from banking software to cloud infrastructure. A deeper understanding of resource reasoning could eventually make the digital systems that underpin modern life—from energy grids to supply chains—more robust without requiring programmers to change how they think.
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