Polynomial loops: beyond termination

DOI10.29007/NXV1MaRDI QIDQ7024202zbMATH OpenFDO

Authors Marcel Hark, Florian Frohn, Jürgen Giesl

Publication date 20 February 2025

Full work available at URL https://doi.org/10.29007/NXV1

zbMATH Keywords

decidabilityhalting problemruntime complexitytermination

Mathematics Subject Classification ID

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

Cites work

• A recursive decision method for termination of linear programs
• Automated resource analysis with Coq proof objects
• Automatic Generation of Polynomial Loop Invariants
• Closed-form upper bounds in static cost analysis
• Complexity and resource bound analysis of imperative programs using difference constraints
• Complexity of Restricted Variants of Skolem and Related Problems
• Complexity verification using guided theorem enumeration
• Computer Aided Verification
• Deciding conditional termination
• Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS
• Invariant generation for multi-path loops with polynomial assignments
• Linear, Polynomial or Exponential? Complexity Inference in Polynomial Time
• Lower runtime bounds for integer programs
• Multiphase-linear ranking functions and their relation to recurrent sets
• Non-termination Sets of Simple Linear Loops
• On termination of integer linear loops
• On the edge of decidability in complexity analysis of loop programs
• On the positivity problem for simple linear recurrence sequences
• Polynomial invariants by linear algebra
• Positivity problems for low-order linear recurrence sequences
• Ranking Templates for Linear Loops
• Reasoning Algebraically About P-Solvable Loops
• Resource analysis driven by (conditional) termination proofs
• Size-Change Abstraction and Max-Plus Automata
• Synthesizing invariants by solving solvable loops
• Termination of Integer Linear Programs
• Termination of linear loops over the integers
• Termination of linear programs with nonlinear constraints
• Termination of single-path polynomial loop programs
• Termination of triangular Integer loops is decidable
• Tight worst-case bounds for polynomial loop programs
• Towards automatic resource bound analysis for OCaml
• Ultimate positivity is decidable for simple linear recurrence sequences
• Witness to non-termination of linear programs

Cited in

(3)

• Termination of triangular polynomial loops
• Targeting completeness: automated complexity analysis of integer programs
• Deciding termination of simple randomized loops

This page was built for publication: Polynomial loops: beyond termination

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