Resource Analysis driven by (Conditional) Termination Proofs

DOI10.1017/S1471068419000152zbMath1434.68101arXiv1907.10096OpenAlexW3101616529WikidataQ113857304 ScholiaQ113857304MaRDI QIDQ5108498

Elvira Albert, Enrique Martin-Martin, Albert Rubio, Cristina Borralleras, Miquel Bofill

Publication date: 4 May 2020

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

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

zbMATH Keywords

upper boundsresource analysistermination analysiscost relation systems

Mathematics Subject Classification ID

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

Related Items (3)

Run-time complexity bounds using squeezers ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes ⋮ Automatic complexity analysis of integer programs via triangular weakly non-linear loops

Uses Software

• AProVE

Cites Work

• Cost analysis of object-oriented bytecode programs
• Resource Analysis of Complex Programs with Cost Equations
• Proving Termination Through Conditional Termination
• Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis
• Mechanical program analysis
• An iterative approach to precondition inference using constrained Horn clauses
• Parallel Cost Analysis

This page was built for publication: Resource Analysis driven by (Conditional) Termination Proofs