{rfName}
In

Indexado en

Licencia y uso

Icono OpenAccess

Citaciones

46

Altmetrics

Investigadores/as Institucionales

Hermenegildo, M., VAutor o Coautor

Compartir

9 de junio de 2019
Publicaciones
>
Artículo
Sí

Interval-based resource usage verification by translation into Horn clauses and an application to energy consumption

Publicado en: THEORY AND PRACTICE OF LOGIC PROGRAMMING. 18 (2): 167-223 - 2018-03-01 18(2), DOI: 10.1017/S1471068418000042

Autores:

Lopez-Garcia, P; Darmawan, L; Klemen, M; Liqat, U; Bueno, F; Hermenegildo, MV
[+]

Afiliaciones

IMDEA Software Inst - Autor o Coautor
Spanish Council Sci Res CSIC - Autor o Coautor
Upm - Autor o Coautor
Ver más

Resumen

Many applications require conformance with specifications that constrain the use of resources, such as execution time, energy, bandwidth, etc. We present a configurable framework for static resource usage verification where specifications can include data size-dependent resource usage functions, expressing both lower and upper bounds. Ensuring conformance with respect to such specifications is an undecidable problem. Therefore, 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 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 intended to hold, proved, or disproved. Most importantly, we also extend the classes of functions that can be checked. We also report on and provide results from an implementation within the Ciao/CiaoPP framework, as well as on a practical tool built by instantiating this framework for the verification of energy consumption specifications for imperative/embedded programs. Finally, we show as an example how embedded software developers can use this tool, in particular, for determining values for program parameters that ensure meeting a given energy budget while minimizing the loss in quality of service.
[+]

Palabras clave

Abstract interpretationCheckingEnergy consumptionHorn clause-based analysis and verificationProgram verification and debuggingResource usage analysis and verificationStatic analysis

Indicios de calidad

Impacto bibliométrico. Análisis de la aportación y canal de difusión

El trabajo ha sido publicado en la revista THEORY AND PRACTICE OF LOGIC PROGRAMMING debido a la progresión y el buen impacto que ha alcanzado en los últimos años, según la agencia WoS (JCR), se ha convertido en una referencia en su campo. En el año de publicación del trabajo, 2018, se encontraba en la posición 1/20, consiguiendo con ello situarse como revista Q1 (Primer Cuartil), en la categoría Logic. Destacable, igualmente, el hecho de que la Revista está posicionada por encima del Percentil 90.

Desde una perspectiva relativa, y atendiendo al indicador del impacto normalizado calculado a partir de las Citas Mundiales proporcionadas por WoS (ESI, Clarivate), arroja un valor para la normalización de citas relativas a la tasa de citación esperada de: 1.25. Esto indica que, de manera comparada con trabajos en la misma disciplina y en el mismo año de publicación, lo ubica como trabajo citado por encima de la media. (fuente consultada: ESI 13 Nov 2025)

De manera concreta y atendiendo a las diferentes agencias de indexación, el trabajo ha acumulado, hasta la fecha 2026-04-09, el siguiente número de citas:

  • WoS: 23
  • Scopus: 22
[+]

Impacto y visibilidad social

Desde la dimensión de Influencia o adopción social, y tomando como base las métricas asociadas a las menciones e interacciones proporcionadas por agencias especializadas en el cálculo de las denominadas “Métricas Alternativas o Sociales”, podemos destacar a fecha 2026-04-09:

  • La utilización de esta aportación en marcadores, bifurcaciones de código, añadidos a listas de favoritos para una lectura recurrente, así como visualizaciones generales, indica que alguien está usando la publicación como base de su trabajo actual. Esto puede ser un indicador destacado de futuras citas más formales y académicas. Tal afirmación es avalada por el resultado del indicador “Capture” que arroja un total de: 6 (PlumX).

Es fundamental presentar evidencias que respalden la plena alineación con los principios y directrices institucionales en torno a la Ciencia Abierta y la Conservación y Difusión del Patrimonio Intelectual. Un claro ejemplo de ello es:

  • El trabajo se ha enviado a una revista cuya política editorial permite la publicación en abierto Open Access.
  • Asignación de un Handle/URN como identificador dentro del Depósito en el Repositorio Institucional: https://oa.upm.es/52885/

Como resultado de la publicación del trabajo en el repositorio institucional, se han obtenido datos estadísticos de uso que reflejan su impacto. En términos de difusión, podemos afirmar que, hasta la fecha

  • Visualizaciones: 326
  • Descargas: 263
[+]

Análisis de liderazgo de los autores institucionales

Existe un liderazgo significativo ya que algunos de los autores pertenecientes a la institución aparecen como primer o último firmante, se puede apreciar en el detalle: Último Autor (HERMENEGILDO SALINAS, MANUEL DE).

[+]

Reconocimientos ligados al ítem

This research was partially funded by EU FP7 318337 ENTRA, Spanish MINECO TIN2012-39391 StrongSoft, and TIN2015-67522-C3-1-R TRACES projects, and the Madrid M141047003 N-GREENS program.
[+]