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

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

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)

Cites Work

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

Cited In (1)

• Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs

Uses Software

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

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

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