June 16, 2015
Maximiliano Klemen
In this talk we will review the general resource analysis framework present in the CiaoPP system. We will start by describing a preliminary version and its evolution that lead to a user-definable resource analysis able to infer both lower and upper bounds on the resources used by program executions. Examples of user-definable resources are energy, bits sent or received by an application over a socket, number of calls to a procedure, number of files left open, number of accesses to a database, monetary units spent, etc., as well as the more traditional execution steps or execution time. Then, we will talk about a recent implementation based on abstract interpretation and the use of sized types, which overcomes some limitations of the previous implementation and related existing approaches, and provides additional advantages. Afterwards, we will show how this resource analyzer is used in combination with CiaoPP’s general framework for resource usage verification in order to estimate and verify the energy consumption of C-like programs. Finally, we will present other recent improvements of key components of the CiaoPP tool.