  Many applications require conformance with specifications that constrain the
use of resources, such as execution time, energy, bandwidth, etc. We have
presented a configurable framework for static resource usage verification where
specifications can include lower and upper bound, data size-dependent resource
usage functions. To statically check such specifications, our framework infers
the same type of resource usage functions, which safely approximate the actual
resource usage of the program, and compares them against the specification. We
review how this framework supports several languages and compilation output
formats by translating them to an intermediate representation based on Horn
clauses and using the configurability of the framework to describe the resource
semantics of the input language. We provide a more detailed formalization and
extend the framework so that both resource usage specification and
analysis/verification output can include preconditions expressing intervals for
the input data sizes for which assertions are applicable, proved, or disproved.
Most importantly, we also extend the classes of functions that can be checked.
We provide results from an implementation within the Ciao/CiaoPP framework, and
report on a tool built by instantiating this framework for the verification of
energy consumption specifications for imperative/embedded programs. This paper
is under consideration for publication in Theory and Practice of Logic
Programming (TPLP).
