Interval-based resource usage verification: Formalization and prototype

López García, Pedro and Darmawan, Luthfi and Bueno Carrillo, Francisco and Hermenegildo, Manuel V. (2011). Interval-based resource usage verification: Formalization and prototype. In: "Second International Workshop, FOPARA 2011", May 19, 2011, Madrid, Spain. ISBN 9783642324949.


Title: Interval-based resource usage verification: Formalization and prototype
  • López García, Pedro
  • Darmawan, Luthfi
  • Bueno Carrillo, Francisco
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: Second International Workshop, FOPARA 2011
Event Dates: May 19, 2011
Event Location: Madrid, Spain
Title of Book: Foundational and Practical Aspects of Resource Analysis
Date: May 2011
ISBN: 9783642324949
Freetext Keywords: Cost analysis, Resource usage analysis, Resource usage verification, Program verification and debugging, Análisis de coste, Análisis del uso de los recursos, Depuración y verificación de programas, Verificacion del uso de los recursos.
Faculty: Facultad de Informática (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview


In an increasing number of applications (e.g., in embedded, real-time, or mobile systems) it is important or even essential to ensure conformance with respect to a specification expressing resource usages, such as execution time, memory, energy, or user-defined resources. In previous work we have presented a novel framework for data size-aware, static resource usage verification. Specifications can include both lower and upper bound resource usage functions. In order to statically check such specifications, both upper- and lower-bound resource usage functions (on input data sizes) approximating the actual resource usage of the program which are automatically inferred and compared against the specification. The outcome of the static checking of assertions can express intervals for the input data sizes such that a given specification can be proved for some intervals but disproved for others. After an overview of the approach in this paper we provide a number of novel contributions: we present a full formalization, and we report on and provide results from an implementation within the Ciao/CiaoPP framework (which provides a general, unified platform for static and run-time verification, as well as unit testing). We also generalize the checking of assertions to allow preconditions expressing intervals within which the input data size of a program is supposed to lie (i.e., intervals for which each assertion is applicable), and we extend the class of resource usage functions that can be checked.

More information

Item ID: 14579
DC Identifier:
OAI Identifier:
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 02 Mar 2013 06:56
Last Modified: 21 Apr 2016 14:18
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM