A Framework for Verification and Debugging of Resource Usage Properties

Bueno Carrillo, Francisco (2010). A Framework for Verification and Debugging of Resource Usage Properties. En: "Technical Communications of the 26th International Conference on Logic Programming, ICLP 2010", 16/07/2010 - 19/07/2010, Edimburgo, UK.

Descripción

Título: A Framework for Verification and Debugging of Resource Usage Properties
Autor/es:
  • Bueno Carrillo, Francisco
Tipo de Documento: Ponencia en Congreso o Jornada (Sin especificar)
Título del Evento: Technical Communications of the 26th International Conference on Logic Programming, ICLP 2010
Fechas del Evento: 16/07/2010 - 19/07/2010
Lugar del Evento: Edimburgo, UK
Título del Libro: Proceedings of Technical Communications of the 26th International Conference on Logic Programming, ICLP 2010
Fecha: 2010
Materias:
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Inteligencia Artificial
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (170kB) | Vista Previa

Resumen

We present a framework for (static) verification of general resource usage program properties. The framework extends the criteria of correctness as the conformance of a program to a specification expressing non-functional global properties, such as upper and lower bounds on execution time, memory, energy, or user defined resources, given as functions on input data sizes. A given specification can include both lower and upper bound resource usage functions, i.e., it can express intervals where the resource usage is supposed to be included in. We have defined an abstract semantics for resource usage properties and operations to compare the (approximated) intended semantics of a program (i.e., the specification) with approximated semantics inferred by static analysis. These operations include the comparison of arithmetic functions (e.g., polynomial, exponential or logarithmic functions). A novel aspect of our framework is that the static checking of assertions generates answers that include conditions under which a given specification can be proved or disproved. For example, these conditions can express intervals of input data sizes such that a given specification can be proved for some intervals but disproved for others. We have implemented our techniques within the Ciao/CiaoPP system in a natural way, so that the novel resource usage verification blends in with the CiaoPP framework that unifies static verification and static debugging (as well as run-time verification and unit testing).

Más información

ID de Registro: 9115
Identificador DC: http://oa.upm.es/9115/
Identificador OAI: oai:oa.upm.es:9115
URL Oficial: http://drops.dagstuhl.de/opus/volltexte/2010/2588/
Depositado por: Memoria Investigacion
Depositado el: 15 Nov 2011 12:05
Ultima Modificación: 20 Abr 2016 17:39
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM