User-Definable Resource Bounds Analysis for Logic Programs

We present a static analysis that infers both upper and lower bounds on the usage that a logic program makes of a set of user-definable resources. The inferred bounds will in general be functions of input data sizes. A resource in our approach is a quite general, user-defined notion which associates a basic cost function with elementary operations. The analysis then derives the related (upper- and lower-bound) resource usage functions for all predicates in the program. We also present an assertion language which is used to define both such resources and resourcerelated properties that the system can then check based on the results of the analysis. We have performed some preliminary experiments with some concrete resources such as execution steps, bytes sent or received by an application, number of files left open, number of accesses to a database, number of calls to a procedure, number of asserts/retracts, etc. Applications of our analysis include resource consumption verification and ...

• Type: Conference
• Year: 2007
• Where: ICLP
• Authors: Jorge Navas, Edison Mera, Pedro López-García, Manuel V. Hermenegildo
• Keywords: Automated Reasoning, Basic Cost Function, ICLP 2007, Resource, Resource Usage Functions