Automated Program Analysis for Bounds on Resource Consumption
Computer programs are consuming physical resources such as time, memory, power and bandwidth. To guarantee that a program only uses a limited amount of these resources, programmers need automated tools which predict the resource consumption of a program. In this project, we will develop such methods and tools for resource prediction.
The starting point of our research is the notion of a "Size Change Abstraction" (SCA). This is a mathematical model that has been successfully used to answer a simpler question about programs - namely, the question if a program runs for a finite amount of time. While Turing has shown that no algorithm can decide this simpler question, there is convincing evidence that SCA allows us to answer it in many practical cases. In a recent paper, we have given a proof of concept that SCA is also highly promising for resource consumption. In this project, we develop both the mathematical methods and the practical software tools to realize this potential of SCA.