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

Many applications require conformance with specifications that constrain theuse of resources, such as execution time, energy, bandwidth, etc. We havepresented a configurable framework for static resource usage verification wherespecifications can include lower and upper bound, data size-dependent resourceusage functions. To statically check such specifications, our framework infersthe same type of resource usage functions, which safely approximate the actualresource usage of the program, and compares them against the specification. Wereview how this framework supports several languages and compilation outputformats by translating them to an intermediate representation based on Hornclauses and using the configurability of the framework to describe the resourcesemantics of the input language. We provide a more detailed formalization andextend the framework so that both resource usage specification andanalysis/verification output can include preconditions expressing intervals forthe 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, andreport on a tool built by instantiating this framework for the verification ofenergy consumption specifications for imperative/embedded programs. This paperis under consideration for publication in Theory and Practice of LogicProgramming (TPLP).

Interval-based Resource Usage Verification by Translation into Horn Clauses and an Application to Energy Consumption