Think about the problem of applying symbolic execution to the problem of energy profiling, specifically estimating envelopes of the min/max number of Joules that a body of code would consume while executing. In order to bootstrap the process, imagine using compositional symbolic execution for this task, and assume the existence of some modules with well understood "summaries" of energy consumption (e.g., device drivers that interact with devices with well known energy characteristics).

Propose a way to use the compositional approach in obtaining a reasonably accurate energy profile for an arbitrary application. What representation would you use for summaries to achieve a good balance between accuracy and scalability of the analysis?