Symbolic Execution for Quantitative Verification of Energy Consumption

We propose a method for verifying a type of non-functional properties related to energy consumption for software in embedded systems. Since these systems are often battery-powered or relying on energy harvesting, it is crucial to analyze and bound energy consumption at design time, yet rigorous methods for doing so are lacking. To solve this problem, we propose a novel integration of three techniques: compiler, symbolic execution, and model counting. Given a C program and the instruction-level power model of a CPU, we can prove that the worst-case energy consumption is below a threshold; otherwise, if this property is violated, we return a counterexample. Our contributions are threefold. First, we extend the LLVM compiler’s code-generation module to map the instruction level power model to LLVM’s intermediate representation (IR). Second, we extend the KLEE symbolic execution tool to leverage the IR-level model to compute the energy to execute each program path. Third, we leverage a model-counting satisfiability solver to compute the probability associated with each program path. In addition to verifying worst-case energy consumption, our method has new capabilities of computing the average energy consumption, and generating a histogram that displays the corresponding probability for each energy level. We have conducted an experimental evaluation on a set of real-time software benchmarks to demonstrate the effectiveness of our method.