Automatic complexity analysis of integer programs via triangular weakly non-linear loops

DOI10.1007/978-3-031-10769-6_43OpenAlexW4289104014MaRDI QIDQ2104561

Jürgen Giesl, Nils Lommen, Fabian Meyer

Publication date: 7 December 2022

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

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Apron
• z3
• TERMINATOR
• TPDB
• KITTeL
• GitHub
• LoAT
• KoAT
• iRankFinder

Cites Work

• Unnamed Item
• Symbolic termination analysis of solvable loops
• On multiphase-linear ranking functions
• Termination of polynomial loops
• Complexity and resource bound analysis of imperative programs using difference constraints
• Resource Analysis of Complex Programs with Cost Equations
• Lower Runtime Bounds for Integer Programs
• Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis
• Automatic Generation of Polynomial Loop Invariants
• Resource Analysis driven by (Conditional) Termination Proofs
• Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis
• Ranking Templates for Linear Loops
• Computer Aided Verification
• Towards automatic resource bound analysis for OCaml
• Termination Analysis of C Programs Using Compiler Intermediate Languages
• Reasoning Algebraically About P-Solvable Loops
• Termination of Integer Linear Programs
• Termination of triangular Integer loops is decidable

This page was built for publication: Automatic complexity analysis of integer programs via triangular weakly non-linear loops