Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913578983882752 |
|---|---|
| author | Lommen, Nils Giesl, Jürgen |
| author_facet | Lommen, Nils Giesl, Jürgen |
| contents | We present a new procedure to infer size bounds for integer programs automatically. Size bounds are important for the deduction of bounds on the runtime complexity or in general, for the resource analysis of programs. We show that our technique is complete (i.e., it always computes finite size bounds) for a subclass of loops, possibly with non-linear arithmetic. Moreover, we present a novel approach to combine and integrate this complete technique into an incomplete approach to infer size and runtime bounds of general integer programs. We prove completeness of our integration for an important subclass of integer programs. We implemented our new algorithm in the automated complexity analysis tool KoAT to evaluate its power, in particular on programs with non-linear arithmetic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2307_06921 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs Lommen, Nils Giesl, Jürgen Logic in Computer Science We present a new procedure to infer size bounds for integer programs automatically. Size bounds are important for the deduction of bounds on the runtime complexity or in general, for the resource analysis of programs. We show that our technique is complete (i.e., it always computes finite size bounds) for a subclass of loops, possibly with non-linear arithmetic. Moreover, we present a novel approach to combine and integrate this complete technique into an incomplete approach to infer size and runtime bounds of general integer programs. We prove completeness of our integration for an important subclass of integer programs. We implemented our new algorithm in the automated complexity analysis tool KoAT to evaluate its power, in particular on programs with non-linear arithmetic. |
| title | Targeting Completeness: Using Closed Forms for Size Bounds of Integer Programs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2307.06921 |