Paper Info
Title
Type-Based Amortized Resource Analysis with Integers and Arrays.
Abstract
Proving bounds on the resource consumption of a program by statically analyzing its source code is an important and well-studied problem. Automatic approaches for numeric programs with side effects usually apply abstract interpretation-based invariant generation to derive bounds on loops and recursion depths of function calls. This paper presents an alternative approach to resource-bound analysis for numeric, heap-manipulating programs that uses type-based amortized resource analysis. As a first step towards the analysis of imperative code, the technique is developed for a first-order ML-like language with unsigned integers and arrays. The analysis automatically derives bounds that are multivariate polynomials in the numbers and the lengths of the arrays in the input. Experiments with example programs demonstrate two main advantages of amortized analysis over current abstract interpretation-based techniques. For one thing, amortized analysis can handle programs with non-linear intermediate values like f ((n + m)(2)). For another thing, amortized analysis is compositional and works naturally for compound programs like f(g(x)).
Year
DOI
Venue
2014
10.1007/978-3-319-07151-0_10
Lecture Notes in Computer Science
Keywords
Field
DocType
Quantitative Analysis,Resource Consumption,Amortized Analysis,Functional Programming,Static Analysis
Integer,Functional programming,Source code,Computer science,Abstract interpretation,Static analysis,Amortized analysis,Algorithm,Theoretical computer science,Invariant (mathematics),Recursion
Conference
Volume
ISSN
Citations 
8475
0302-9743
8
PageRank 
References 
Authors
0.46
19
2
Name
Order
Citations
PageRank
Jan Hoffmannand120316.61
Zhong Shao289768.80