Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(12)
Experimental Validation
Functional Language
Functional Programming
Linear Operator
Longest Common Subsequence
Multivariate Polynomial
Quantitative Analysis
Static Analysis
Type Inference
Type System
First Order
Linear Program
Subscribe
Academic
Publications
Multivariate amortized resource analysis
Multivariate amortized resource analysis,10.1145/1925844.1926427,Sigplan Notices,Jan Hoffmann,Klaus Aehlig,Martin Hofmann
Edit
Multivariate amortized resource analysis
(
Citations: 2
)
BibTex

RIS

RefWorks
Download
Jan Hoffmann
,
Klaus Aehlig
,
Martin Hofmann
We study the problem of automatically analyzing the worstcase resource usage of procedures with several arguments. Existing automatic analyses based on amortization, or sized types bound the resource usage or result size of such a procedure by a sum of unary functions of the sizes of the arguments. In this paper we generalize this to arbitrary
multivariate polynomial
functions thus allowing bounds of the form mn which had to be grossly overestimated by m2+n2 before. Our framework even encompasses bounds like ∗i,j≤n m_i mj where the mi are the sizes of the entries of a list of length n. This allows us for the first time to derive useful resource bounds for operations on matrices that are represented as lists of lists and to considerably improve bounds on other superlinear operations on lists such as
longest common subsequence
and removal of duplicates from lists of lists. Furthermore, resource bounds are now closed under composition which improves accuracy of the analysis of composed programs when some or all of the components exhibit superlinear resource or size behavior. The analysis is based on a novel multivariate amortized resource analysis. We present it in form of a
type system
for a simple firstorder
functional language
with lists and trees, prove soundness, and describe automatic
type inference
based on linear programming. We have experimentally validated the automatic analysis on a wide range of examples from
functional programming
with lists and trees. The obtained bounds were compared with actual resource consumption. All bounds were asymptotically tight, and the constants were close or even identical to the optimal ones.
Journal:
Sigplan Notices  SIGPLAN
, pp. 357370, 2011
DOI:
10.1145/1925844.1926427
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
dl.acm.org
)
(
portal.acm.org
)
(
portal.acm.org
)
Citation Context
(2)
...Good examples are type systems for amortized analysis [5], [
21
] or those using ideas from linear logic [8], [9]...
Ugo Dal Lago
,
et al.
Linear Dependent Types and Relative Completeness
...A cost analysis for Java bytecode has been developed in [2], for C++ in [12], and for functional programs in [
13
]...
...The analysis of [
13
] supports inference of memory usage, and accounts for memory freed by destructive matching...
Elvira Albert
,
et al.
Simulating Concurrent Behaviors with WorstCase Cost Bounds
References
(26)
Cost Analysis of Java Bytecode
(
Citations: 63
)
Elvira Albert
,
Puri Arenas
,
Samir Genaim
,
Germán Puebla
,
Damiano Zanardini
Conference:
European Symposium on Programming  ESOP
, pp. 157172, 2007
Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis
(
Citations: 33
)
Elvira Albert
,
Puri Arenas
,
Samir Genaim
,
Germán Puebla
Conference:
Static Analysis Symposium/Workshop on Static Analysis  SAS(WSA)
, pp. 221237, 2008
Amortised Resource Analysis with Separation Logic
(
Citations: 5
)
Robert Atkey
Conference:
European Symposium on Programming  ESOP
, pp. 85103, 2010
Automated higherorder complexity analysis
(
Citations: 21
)
Ralph Benzinger
Journal:
Theoretical Computer Science  TCS
, vol. 318, no. 12, pp. 79103, 2004
Automatic Certification of Heap Consumption
(
Citations: 37
)
Lennart Beringer
,
Martin Hofmann
,
Alberto Momigliano
,
Olha Shkaravska
Conference:
Logic Programming and Automated Reasoning/Russian Conference on Logic Programming  LPAR(RCLP)
, pp. 347362, 2004
Sort by:
Citations
(2)
Linear Dependent Types and Relative Completeness
(
Citations: 1
)
Ugo Dal Lago
,
Marco Gaboardi
Conference:
Logic in Computer Science  LICS
, vol. abs/1104.0, pp. 133142, 2011
Simulating Concurrent Behaviors with WorstCase Cost Bounds
(
Citations: 1
)
Elvira Albert
,
Samir Genaim
,
Miguel GómezZamalloa
,
Einar Broch Johnsen
,
Rudolf Schlatte
,
S. Tarifa