Energy consumption analysis and verification by transformantion into horn clauses and abstract interpretation

The static estimation of the energy consumed by program executions has applications in program optimization and verification, and is instrumental in energy-aware software development. We describe our approach for estimating such energy consumption statically (i.e., at compile-time, without running the program) in the form of functions on the input data sizes of procedures (and possibly other hardwaredependent parameters), and for using such functions for verifying and finding errors with respect to a rich class of energy consumption specifications for programs. We also present the implementation of this approach within the CiaoPP system