TU Darmstadt / ULB / TUbiblio

Resource Analysis of Complex Programs with Cost Equations

Flores-Montoya, Antonio and Hähnle, Reiner (2014):
Resource Analysis of Complex Programs with Cost Equations.
[Report]

Abstract

We present a novel static analysis for inferring precise complexity bounds of imperative and recursive programs. The analysis operates on cost equations. Therefore, it permits uniform treatment of loops and recursive procedures. The analysis is able to provide precise upper bounds for programs with complex execution flow and multi-dimensional ranking functions. In a first phase, a combination of control-flow refinement and invariant generation creates a representation of the possible behaviors of a (possibly inter-procedural) program in the form of a set of execution patterns. In a second phase, a cost upper bound of each pattern is obtained by combining individual costs of code fragments. Our technique is able to detect dependencies between different pieces of code and hence to compute a precise upper bounds for a given program. A prototype has been implemented and evaluated to demonstrate the effectiveness of the approach.

Item Type: Report
Erschienen: 2014
Creators: Flores-Montoya, Antonio and Hähnle, Reiner
Title: Resource Analysis of Complex Programs with Cost Equations
Language: German
Abstract:

We present a novel static analysis for inferring precise complexity bounds of imperative and recursive programs. The analysis operates on cost equations. Therefore, it permits uniform treatment of loops and recursive procedures. The analysis is able to provide precise upper bounds for programs with complex execution flow and multi-dimensional ranking functions. In a first phase, a combination of control-flow refinement and invariant generation creates a representation of the possible behaviors of a (possibly inter-procedural) program in the form of a set of execution patterns. In a second phase, a cost upper bound of each pattern is obtained by combining individual costs of code fragments. Our technique is able to detect dependencies between different pieces of code and hence to compute a precise upper bounds for a given program. A prototype has been implemented and evaluated to demonstrate the effectiveness of the approach.

Divisions: 20 Department of Computer Science
20 Department of Computer Science > Software Engineering
Date Deposited: 31 Dec 2016 10:40
Identification Number: TUD-CS-2014-0903
Related URLs:
Export:

Optionen (nur für Redakteure)

View Item View Item