Go to page
 

Bibliographic Metadata

Title
Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints
AuthorSinn, Moritz ; Zuleger, Florian ; Veith, Helmut
Published in
Journal of Automated Reasoning, 2017, Vol. 59, Issue 1, page 3-45
PublishedSpringer Nature, 2017
LanguageEnglish
Document typeJournal Article
Keywords (EN)Bound analysis / Complexity analysis / Amortized analysis / Difference constraints / Static analysis / Resource bound analysis / Automatic complexity analysis / Cost analysis
ISSN1573-0670
URNurn:nbn:at:at-ubtuw:3-4002 Persistent Identifier (URN)
DOI10.1007/s10817-016-9402-4 
Restriction-Information
 The work is publicly available
Files
Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints [1.71 mb]Supplementary Material [0.29 mb]
Links
Reference
Classification
Abstract (English)

Difference constraints have been used for termination analysis in the literature, where they denote relational inequalities of the form x′y+c, and describe that the value of x in the current state is at most the value of y in the previous state plus some constant cZ. We believe that difference constraints are also a good choice for complexity and resource bound analysis because the complexity of imperative programs typically arises from counter increments and resets, which can be modeled naturally by difference constraints. In this article we propose a bound analysis based on difference constraints. We make the following contributions: (1) our analysis handles bound analysis problems of high practical relevance which current approaches cannot handle: we extend the range of bound analysis to a class of challenging but natural loop iteration patterns which typically appear in parsing and string-matching routines. (2) We advocate the idea of using bound analysis to infer invariants: our soundness proven algorithm obtains invariants through bound analysis, the inferred invariants are in turn used for obtaining bounds. Our bound analysis therefore does not rely on external techniques for invariant generation. (3) We demonstrate that difference constraints are a suitable abstract program model for automatic complexity and resource bound analysis: we provide efficient abstraction techniques for obtaining difference constraint programs from imperative code. (4) We report on a thorough experimental comparison of state-of-the-art bound analysis tools: we set up a tool comparison on (a) a large benchmark of real-world C code, (b) a benchmark built of examples taken from the bound analysis literature and (c) a benchmark of challenging iteration patterns which we found in real source code. (5) Our analysis is more scalable than existing approaches: we discuss how we achieve scalability.

Stats
The PDF-Document has been downloaded 7 times.
License
CC-BY-License (4.0)Creative Commons Attribution 4.0 International License