Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis

DOI10.1007/978-3-540-69166-2_15MaRDI QIDQ3522073zbMATH OpenOpenAlexFDO

Authors Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla

Publication date 28 August 2008

Published in Static Analysis (Search for Journal in Brave)

Full work available at URL http://oa.upm.es/2904/

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Closed-form upper bounds in static cost analysis
• On the inference of resource usage upper and lower bounds
• More precise yet widely applicable cost analysis
• Resource analysis of complex programs with cost equations
• Precise cost analysis via local reasoning

Cites work

• scientific article; zbMATH DE number 3716758 (Why is no real title available?)
• scientific article; zbMATH DE number 1948398 (Why is no real title available?)
• scientific article; zbMATH DE number 236855 (Why is no real title available?)
• A Naïve Time Analysis and its Theory of Cost Equivalence
• Automated higher-order complexity analysis
• Automating program analysis
• Mechanical program analysis
• Programming Languages and Systems
• Resource Analysis by Sup-interpretation
• Resource bound certification
• Static prediction of heap space usage for first-order functional programs

Cited in

(16)

• Automatic complexity analysis of integer programs via triangular weakly non-linear loops
• Lower-bound synthesis using loop specialization and Max-SMT
• Verification of gap-order constraint abstractions of counter systems
• Closed-form upper bounds in static cost analysis
• Run-time complexity bounds using squeezers
• On the inference of resource usage upper and lower bounds
• Runtime complexity analysis of logically constrained rewriting
• Interpolation-based height analysis for improving a recurrence solver
• Control-flow refinement for complexity analysis of probabilistic programs in \textsf{KoAT} (short paper)
• Automated recurrence analysis for almost-linear expected-runtime bounds
• Resource analysis driven by (conditional) termination proofs
• Targeting completeness: automated complexity analysis of integer programs
• Cost recurrences for DML programs
• Quantified abstract configurations of distributed systems
• More precise yet widely applicable cost analysis
• Type-based analysis of logarithmic amortised complexity

Describes a project that uses

Uses Software

• PURRS

This page was built for publication: Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis

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