PI: Wojciech Mostowski (HH); co-PI Christoph Reichenbach (LU)
This project focuses on developing new methods in static analysis to achieve verifiable energy efficiency of software. Research on energy efficiency typically focuses on hardware, but a lavishly designed or buggy program can easily waste the hardware design efforts by being unaware of the energy consumption intricacies of the execution platform. To help capture energy consumption requirements and guarantees for software, we will develop specific program annotations in design-by-contract style that take into account power consumption of the underlying program constructs, from single statement up to complete procedures. We then propose two different static analysis methods of different precision, working in separation or combination, to help in (i) verifying the annotations, and in (ii) proposing candidate annotations. When verification succeeds, power consumption annotations give quantified statements about energy efficiency. When verification fails, the failure can point to power consumption related bugs, e.g., so-called resource leaks. Combined with platform-specific power consumption models, we can then derive absolute statements about power consumption (on platform X the program uses at most Y power), or relative statements (program A is more energy efficient than program B). One of the prerequisites for such analysis is a suitable power profile of the execution platform to be developed early in the project. Our research will be supported by suitable and realistic case studies where appropriate.
Project number: D12