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

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 sed 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 condi...

• Type: Journal
• Year: 2010
• Where: ICLP
• Authors: Pedro López-García, Luthfi Darmawan, Francisco Bueno
• Keywords: Automated Reasoning, ICLP 2010, Input Data, Resource Usage, Specification