A Framework for Verification and Debugging of Resource Usage Properties: Resource Usage Verification

Authors Pedro Lopez-Garcia, Luthfi Darmawan, Francisco Bueno



PDF
Thumbnail PDF

File

LIPIcs.ICLP.2010.104.pdf
  • Filesize: 349 kB
  • 10 pages

Document Identifiers

Author Details

Pedro Lopez-Garcia
Luthfi Darmawan
Francisco Bueno

Cite As Get BibTex

Pedro Lopez-Garcia, Luthfi Darmawan, and Francisco Bueno. A Framework for Verification and Debugging of Resource Usage Properties: Resource Usage Verification. In Technical Communications of the 26th International Conference on Logic Programming. Leibniz International Proceedings in Informatics (LIPIcs), Volume 7, pp. 104-113, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010) https://doi.org/10.4230/LIPIcs.ICLP.2010.104

Abstract

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).

Subject Classification

Keywords
  • Program Verification and Debugging
  • Cost Analysis
  • Resource Usage Analysis
  • Complexity Analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail