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

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

Authors: Nils Lommen, Fabian Meyer, Jürgen Giesl 

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

• 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
• Title not available (Why is that?)
• 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)