Accelerating Loops with Arrays
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910235231256576 |
|---|---|
| author | Frohn, Florian Giesl, Jürgen |
| author_facet | Frohn, Florian Giesl, Jürgen |
| contents | We propose a novel acceleration technique for loops operating on arrays. The goal of acceleration is to characterize the transitive closure of loops in a logic which is suitable for automated reasoning. Using the new notion of inductive lvalues, our technique can handle loops where previous techniques fail, and it unifies acceleration for arrays and scalar variables by regarding scalars as arrays of dimension 0. Moreover, our approach uses λs instead of quantifiers. Then the resulting SMT problems can be solved via lemmas on demand. An empirical evaluation of our implementation in the tool LoAT shows the power of our approach. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_19499 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Accelerating Loops with Arrays Frohn, Florian Giesl, Jürgen Logic in Computer Science We propose a novel acceleration technique for loops operating on arrays. The goal of acceleration is to characterize the transitive closure of loops in a logic which is suitable for automated reasoning. Using the new notion of inductive lvalues, our technique can handle loops where previous techniques fail, and it unifies acceleration for arrays and scalar variables by regarding scalars as arrays of dimension 0. Moreover, our approach uses λs instead of quantifiers. Then the resulting SMT problems can be solved via lemmas on demand. An empirical evaluation of our implementation in the tool LoAT shows the power of our approach. |
| title | Accelerating Loops with Arrays |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2605.19499 |