Lower runtime bounds for integer programs

DOI10.1007/978-3-319-40229-1_37MaRDI QIDQ2817952zbMATH OpenOpenAlexFDO

Authors Florian Frohn, Matthias Naaf, Jera Hensel, Marc Brockschmidt, Jürgen Giesl

Publication date 5 September 2016

Published in Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1911.01077

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Integer programming (90C10)

Abstract: We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs, where in contrast to earlier work, our approach is not restricted to tail-recursion. Our technique constructs symbolic representations of program executions using a framework for iterative, under-approximating program simplification. The core of this simplification is a method for (under-approximating) program acceleration based on recurrence solving and a variation of ranking functions. Afterwards, we deduce asymptotic lower bounds from the resulting simplified programs using a special-purpose calculus and an SMT encoding. We implemented our technique in our tool LoAT and show that it infers non-trivial lower bounds for a large class of examples.

Recommendations

• Inferring lower bounds for runtime complexity
• Lower bounds for runtime complexity of term rewriting
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• On the inference of resource usage upper and lower bounds
• Lower-bound synthesis using loop specialization and Max-SMT

Cites work

• Abstract acceleration of general linear loops
• Combining Widening and Acceleration in Linear Relation Analysis
• Computer Aided Verification
• Inferring lower bounds for runtime complexity
• Lower runtime bounds for integer programs
• Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs
• Multivariate amortized resource analysis
• On the inference of resource usage upper and lower bounds
• Resource analysis of complex programs with cost equations
• Under-approximating loops in C programs for fast counterexample detection
• Verification, Model Checking, and Abstract Interpretation

Cited in

(12)

• Proving non-termination and lower runtime bounds with \textsf{LoAT} (system description)
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Automatic complexity analysis of integer programs via triangular weakly non-linear loops
• Lower-bound synthesis using loop specialization and Max-SMT
• Lower runtime bounds for integer programs
• A calculus for modular loop acceleration
• From Jinja bytecode to term rewriting: a complexity reflecting transformation
• Polynomial loops: beyond termination
• Inferring lower bounds for runtime complexity
• Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
• Lower bounds for runtime complexity of term rewriting

Describes a project that uses

Uses Software

• GitHub
• LoAT
• PURRS
• Aspic
• z3
• Apron

This page was built for publication: Lower runtime bounds for integer programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2817952)