English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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. Determining program energy consumption requires the analysis of low-level program representations, since sufficiently accurate energy models are only available at the instruction set architecture level or, with some precision loss, at intermediate levels (such as, e.g., LLVM). We have developed an approach to the analysis and verification of energy consumption [14, 8, 10, 7, 6] that is based on a transformation of instruction set architecture(or LLVM-)level programs into Horn clauses [13, 4]. The Horn clauses encode the semantics of these low-level programs, at different levels of abstraction, as determined by different abstract domains. Such abstract domains approximate properties that are instrumental for energy analysis, such as sized types, determinacy, or non-failure, as well as the energy consumption itself [17]. The latter contrasts with previous approaches to cost analysis that are not based directly on abstract interpretation. Given such a set of Horn clauses, the objective of our analysis is to compute their abstract minimal model for each abstract domain or combination of domains. For this purpose we use the PLAI analyzer of the CiaoPP system [5]. PLAI computes the abstract minimal model of a set of Horn clauses using a topdown, memo table-based fixpoint algorithm –which can be seen as an extension of a highly optimized SLDT resolution engine with the abstract domains taking the traditional role of constraint domains in

Energy Consumption Analysis and Verification by Transformation into Horn Clauses and Abstract Interpretation