Conference paperFIEDOR Tomáš, HOLÍK Lukáš, ROGALEWICZ Adam, SINN Moritz, VOJNAR Tomáš and ZULEGER Florian. From Shapes to Amortized Complexity. In: Proceedings of VMCAI'18. Heidelberg: Springer Verlag, 2018, pp. 205225. ISBN 9783319737201. ISSN 03029743. Available from: https://link.springer.com/chapter/10.1007%2F9783319737218_10  Publication language:  english 

Original title:  From Shapes to Amortized Complexity 

Title (cs):  Od Tvarů K Amortizované Složitosti 

Pages:  205225 

Proceedings:  Proceedings of VMCAI'18 

Conference:  International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2018)/Symposium on Principles of Programming Languages (POPL 2018) 

Series:  Lecture Notes in Computer Science 10145 

Place:  Heidelberg, DE 

Year:  2018 

URL:  https://link.springer.com/chapter/10.1007%2F9783319737218_10 

ISBN:  9783319737201 

Journal:  Lecture Notes in Computer Science, No. 10747, DE 

ISSN:  03029743 

DOI:  10.1007/9783319737218_10 

Publisher:  Springer Verlag 

Keywords 

program analysis, shape analysis, forest automata, tree automata, resource bounds analysis, amortized complexity 
Annotation 

We propose a new method for the automated resource bound analysis of programs manipulating dynamic data structures built on top of an underlying shape and resource bound analysis. Our approach first constructs an integer abstraction for the input program using information gathered by a shape analyser; then a resource bound analyzer is run on the resulting integer program. The integer abstraction is based on shape normsnumerical measures on dynamic data structures (e.g., the length of a linked list). In comparison to related approaches, we consider a larger class of shape norms which we derive by a lightweight program analysis. The analysis identifies paths through the involved dynamic data structures, and filters the norms which are unlikely to be useful for the later bound analysis. We present a calculus for deriving the numeric changes of the shape norms, thereby generating the integer program. Our calculus encapsulates the minimal information which is required from the shape analysis. We have implemented our approach on top of the Forester shape analyser and evaluated it on a number of programs manipulating various list and tree structures using the Loopus tool as the underlying bounds analyser. We report on programs with complex data structures and/or using complex algorithms that could not be analysed in a fully automated and precise way before. 
BibTeX: 

@INPROCEEDINGS{
author = {Tom{\'{a}}{\v{s}} Fiedor and Luk{\'{a}}{\v{s}}
Hol{\'{i}}k and Adam Rogalewicz and Moritz Sinn
and Tom{\'{a}}{\v{s}} Vojnar and Florian Zuleger},
title = {From Shapes to Amortized Complexity},
pages = {205225},
booktitle = {Proceedings of VMCAI'18},
series = {Lecture Notes in Computer Science 10145},
journal = {Lecture Notes in Computer Science},
number = {10747},
year = {2018},
location = {Heidelberg, DE},
publisher = {Springer Verlag},
ISBN = {9783319737201},
ISSN = {03029743},
doi = {10.1007/9783319737218_10},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php?id=11561}
} 
