Complexity and resource bound analysis of imperative programs using difference constraints

DOI10.1007/s10817-016-9402-4zbMath1409.68076OpenAlexW2577171054WikidataQ58105348 ScholiaQ58105348MaRDI QIDQ2398171

Florian Zuleger, Helmut Veith, Moritz Sinn

Publication date: 15 August 2017

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-016-9402-4

zbMATH Keywords

cost analysisstatic analysiscomplexity analysisbound analysisamortized analysisdifference constraintsautomatic complexity analysisresource bound analysis

Mathematics Subject Classification ID

Related Items (17)

ATLAS: automated amortised complexity analysis of self-adjusting data structures ⋮ Lower-bound synthesis using loop specialization and Max-SMT ⋮ Selectively-amortized resource bounding ⋮ Complexity and resource bound analysis of imperative programs using difference constraints ⋮ Rely-guarantee termination and cost analyses of loops with concurrent interleavings ⋮ Exponential automatic amortized resource analysis ⋮ The polynomial complexity of vector addition systems with states ⋮ Unnamed Item ⋮ Run-time complexity bounds using squeezers ⋮ Certified abstract cost analysis ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free ⋮ Automatic complexity analysis of integer programs via triangular weakly non-linear loops ⋮ Relational cost analysis in a functional-imperative setting ⋮ Type-based analysis of logarithmic amortised complexity

Uses Software

• LLVM
• SPEED
• Easychair
• GitHub

Cites Work

• A new look at the automatic synthesis of linear ranking functions
• Cost analysis of object-oriented bytecode programs
• Complexity and resource bound analysis of imperative programs using difference constraints
• Resource Analysis of Complex Programs with Cost Equations
• Size-Change Abstraction and Max-Plus Automata
• On the Foundations of Quantitative Information Flow
• Amortized Computational Complexity
• Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
• Automatic numeric abstractions for heap-manipulating programs
• SPEED
• A combination framework for tracking partition sizes
• Multivariate amortized resource analysis
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Complexity and resource bound analysis of imperative programs using difference constraints