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

DOI10.1007/978-3-031-10769-6_43MaRDI QIDQ2104561zbMATH OpenOpenAlexFDO

Authors Nils Lommen, Fabian Meyer, Jürgen Giesl

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

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

• scientific article; zbMATH DE number 7561611 (Why is no real title available?)
• Automatic Generation of Polynomial Loop Invariants
• Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis
• Complexity and resource bound analysis of imperative programs using difference constraints
• Computer Aided Verification
• Control-flow refinement by partial evaluation, and its application to termination and cost analysis
• Lower runtime bounds for integer programs
• On multiphase-linear ranking functions
• Ranking Templates for Linear Loops
• Reasoning Algebraically About P-Solvable Loops
• Resource analysis driven by (conditional) termination proofs
• Resource analysis of complex programs with cost equations
• Symbolic termination analysis of solvable loops
• Termination Analysis of C Programs Using Compiler Intermediate Languages
• Termination of Integer Linear Programs
• Termination of polynomial loops
• Termination of triangular Integer loops is decidable
• Towards automatic resource bound analysis for OCaml

Cited in

(1)

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

Describes a project that uses

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)