Targeting Completeness: Automated Complexity Analysis of Integer Programs
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913986024308736 |
|---|---|
| author | Lommen, Nils Meyer, Éléanore Giesl, Jürgen |
| author_facet | Lommen, Nils Meyer, Éléanore Giesl, Jürgen |
| contents | There exist several approaches to infer runtime or resource bounds for integer programs automatically. In this paper, we study the subclass of periodic rational solvable loops (prs-loops), where questions regarding the runtime and the size of variable values are decidable and where we can therefore obtain techniques that are complete for such subclasses. We show how to use these results for the complexity analysis of arbitrary general integer programs. To this end, we present a modular approach which computes local runtime and size bounds for subprograms which correspond to prs-loops. These local bounds are then lifted to global runtime and size bounds for the whole integer program. Furthermore, we introduce several techniques to transform larger programs into prs-loops to increase the scope of the approach. The power of the procedure is shown by our implementation in the complexity analysis tool KoAT. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_01832 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Targeting Completeness: Automated Complexity Analysis of Integer Programs Lommen, Nils Meyer, Éléanore Giesl, Jürgen Logic in Computer Science There exist several approaches to infer runtime or resource bounds for integer programs automatically. In this paper, we study the subclass of periodic rational solvable loops (prs-loops), where questions regarding the runtime and the size of variable values are decidable and where we can therefore obtain techniques that are complete for such subclasses. We show how to use these results for the complexity analysis of arbitrary general integer programs. To this end, we present a modular approach which computes local runtime and size bounds for subprograms which correspond to prs-loops. These local bounds are then lifted to global runtime and size bounds for the whole integer program. Furthermore, we introduce several techniques to transform larger programs into prs-loops to increase the scope of the approach. The power of the procedure is shown by our implementation in the complexity analysis tool KoAT. |
| title | Targeting Completeness: Automated Complexity Analysis of Integer Programs |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2412.01832 |