Accelerating Loops with Arrays

Florian Frohn; J\"urgen Giesl

arxiv: 2605.19499 · v1 · pith:ESGM7J6Jnew · submitted 2026-05-19 · 💻 cs.LO

Accelerating Loops with Arrays

Florian Frohn , J\"urgen Giesl This is my paper

Pith reviewed 2026-05-20 02:22 UTC · model grok-4.3

classification 💻 cs.LO

keywords loop accelerationarray programsinductive lvaluestransitive closureSMT solvingprogram verificationlambda termsautomated reasoning

0 comments

The pith

A new acceleration technique for array loops uses inductive lvalues and lambda terms to characterize transitive closures.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a method to express the net effect of repeated loop iterations on arrays in a form that automated reasoners can handle directly. This matters for verifying programs that repeatedly update array elements, where simulating each step is infeasible. The approach introduces inductive lvalues to capture array updates that previous methods could not, and it treats ordinary scalar variables uniformly as arrays of dimension zero. Instead of quantifiers, the method relies on lambda expressions so that SMT solvers can discharge the resulting problems with lemmas on demand. An implementation inside the LoAT tool provides evidence that the technique succeeds on loops that earlier acceleration methods miss.

Core claim

The central claim is that inductive lvalues permit a transitive-closure characterization of array-manipulating loops inside a lambda-based logic; the same representation applies to scalar variables when they are viewed as zero-dimensional arrays, and the resulting SMT queries become solvable by lemmas on demand without explicit quantifiers.

What carries the argument

Inductive lvalues, a new notion that records how array positions are updated across iterations so that the overall effect after any number of steps can be expressed directly.

If this is right

Loops previously out of reach for acceleration become amenable to automated analysis.
Scalar-variable acceleration is recovered as the special case of zero-dimensional arrays.
Quantifier-free lambda encodings replace quantified formulas, shifting the burden to lemma generation inside SMT solvers.
The same framework can be implemented once and applied uniformly to both arrays and scalars.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The technique may extend to other mutable data structures whose updates can be captured by similar indexed identities.
Integration with existing program verifiers could reduce the need for manual invariants on array-heavy code.
Because scalars are handled identically to arrays, the method offers a uniform implementation target for mixed scalar-array programs.

Load-bearing premise

That every loop under consideration admits a transitive-closure representation built from inductive lvalues and lambda terms whose correctness SMT solvers can verify via lemmas on demand.

What would settle it

An array loop whose transitive closure cannot be expressed using inductive lvalues and lambda terms, or for which the corresponding SMT problem remains unsolved after reasonable lemma-generation effort.

read the original abstract

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 {\lambda}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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This extends loop acceleration to arrays with inductive lvalues and lambdas, unifying scalars as zero-dimensional cases and showing gains on prior intractable examples in LoAT.

read the letter

The punchline is that this paper presents a way to accelerate loops involving arrays by defining inductive lvalues and representing the effects with lambda terms rather than quantifiers. This lets it handle cases that scalar-only methods miss and treats scalars as zero-dimensional arrays for a unified approach. The new part is the combination of inductive lvalues with the lambda-based encoding. Prior work on loop acceleration focused on scalars or had trouble with arrays, so this fills a gap in automated reasoning for programs that use array updates. The empirical evaluation in the LoAT tool is a plus, as it shows the method working on examples where earlier techniques failed. The approach looks solid in avoiding circular definitions and building on SMT solvers with lemmas on demand. That setup keeps things practical for verification tasks. A soft spot could be the generality of the inductive lvalues. The stress-test raises the issue of whether they correctly capture transitive closures when array indices depend on previous loop iterations in non-simple ways. If the rules implicitly require affine or monotonic indices, the claim of handling previously intractable loops might not hold as broadly as stated. The paper would be stronger with explicit discussion of the index expression classes it supports and any counterexamples it rules out. This kind of work is aimed at the community doing program analysis and termination proving with SMT. A reader who needs to extend existing accelerators to real code with arrays would get direct value from the unification idea and the lambda trick. I recommend sending it for peer review. The idea is a clear step forward with an implementation backing it up, so referees can check the details and suggest improvements.

Referee Report

2 major / 2 minor

Summary. The paper proposes a novel acceleration technique for loops operating on arrays. Using the new notion of inductive lvalues, the method characterizes the transitive closure of such loops in a logic suitable for automated reasoning. It handles loops where previous techniques fail, unifies acceleration for arrays and scalar variables by treating scalars as arrays of dimension 0, and employs λ-terms instead of quantifiers so that the resulting SMT problems can be solved via lemmas on demand. An empirical evaluation in the LoAT tool demonstrates the approach on previously intractable examples.

Significance. If the central claims hold, this advances loop acceleration in automated program verification by extending it to array-manipulating programs, a common but difficult case. The unification of scalars and arrays via dimension-0 arrays and the shift to λ-terms for quantifier-free SMT discharge are conceptually clean contributions that could improve completeness in tools relying on transitive-closure characterizations.

major comments (2)

[§3] §3 (Inductive Lvalues): The soundness argument for inductive lvalues as a transitive-closure characterization must explicitly address array updates whose indices depend on values computed in prior iterations. The current presentation appears to assume index expressions remain independent of the array state across iterations; a counterexample or formal lemma showing preservation under data-dependent indexing is required, as this is load-bearing for the claim of handling loops that prior techniques cannot.
[§4.2] §4.2 (λ-term encoding): The claim that the λ-based encoding avoids quantifiers while remaining expressible in the SMT fragment used by lemmas-on-demand needs a precise statement of the target logic and a proof that the encoding is equisatisfiable with the original quantified transitive closure. Without this, it is unclear whether the approach is strictly stronger than existing quantifier-based accelerations.

minor comments (2)

[Abstract / §1] The abstract and introduction should cite the specific prior acceleration techniques (e.g., the works on scalar loop acceleration) that are claimed to fail on the new examples, with a brief comparison table.
[§2] Notation for lvalues and λ-abstractions should be introduced with a small running example before the general definitions to improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. We address each major comment below, clarifying the relevant sections and committing to revisions that strengthen the presentation without altering the core claims.

read point-by-point responses

Referee: [§3] The soundness argument for inductive lvalues as a transitive-closure characterization must explicitly address array updates whose indices depend on values computed in prior iterations. The current presentation appears to assume index expressions remain independent of the array state across iterations; a counterexample or formal lemma showing preservation under data-dependent indexing is required.

Authors: We agree that the soundness argument benefits from an explicit treatment of data-dependent indexing. The inductive lvalue definition in §3 is formulated to permit index expressions that may depend on prior array states via the recursive characterization. To make this rigorous, the revised manuscript will add Lemma 3.5, which proves that the transitive-closure property is preserved under such updates. The lemma will include a proof sketch and a concrete example of a loop with data-dependent indexing that prior techniques cannot handle. revision: yes
Referee: [§4.2] The claim that the λ-based encoding avoids quantifiers while remaining expressible in the SMT fragment used by lemmas-on-demand needs a precise statement of the target logic and a proof that the encoding is equisatisfiable with the original quantified transitive closure. Without this, it is unclear whether the approach is strictly stronger than existing quantifier-based accelerations.

Authors: We accept that §4.2 would be improved by additional formality. The revised version will state the target logic as the quantifier-free fragment of the extensional array theory augmented with λ-abstractions (the fragment for which modern SMT solvers support lemma-on-demand instantiation). We will also add a theorem establishing equisatisfiability between the λ-encoding and the original quantified characterization, together with a proof outline that any satisfying assignment for the λ-formula corresponds to a model of the quantified transitive closure. This does not claim strict superiority over quantifier-based methods but demonstrates practical advantages for lemma-on-demand solving. revision: yes

Circularity Check

0 steps flagged

No significant circularity; inductive lvalues introduced as independent syntactic notion for transitive closure

full rationale

The paper introduces the new notion of inductive lvalues as a syntactic device to express transitive closures of array-updating loops without quantifiers, using λ-terms instead. This is positioned as an extension of prior SMT-based acceleration techniques rather than a redefinition of the target property. The central derivation proceeds by defining inductive lvalues, showing they capture the effect of repeated array writes, and reducing the resulting formulas to lemmas discharged by external SMT solvers. No step equates the claimed acceleration result to a fitted parameter, a self-referential definition, or a load-bearing self-citation whose content is merely renamed. The approach is self-contained against the external benchmark of existing loop-acceleration literature and SMT decision procedures.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

Only the abstract is available, so no concrete free parameters, axioms, or invented entities can be extracted from the full manuscript.

axioms (1)

domain assumption Loops admit a transitive-closure characterization in a logic suitable for automated reasoning
Stated as the goal of acceleration in the abstract.

invented entities (1)

inductive lvalues no independent evidence
purpose: To capture array-element updates across loop iterations
Presented as the key new notion enabling the technique

pith-pipeline@v0.9.0 · 5613 in / 1179 out tokens · 45572 ms · 2026-05-20T02:22:46.352357+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages · 1 internal anchor

[1]

In: FroCoS 13

Alberti, F., Ghilardi, S., Sharygina, N.: Definability of accelerated relations in a theory of arrays and its applications. In: FroCoS 13. pp. 23–39. LNCS 8152 (2013). https://doi.org/10.1007/978-3-642-40885-4 3

work page doi:10.1007/978-3-642-40885-4 2013
[2]

Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. J. Autom. Reason.54(4), 327–352 (2015). https://doi.org/10.1007/ S10817-015-9323-7

work page 2015
[3]

In: FroCoS 15

Alberti, F., Ghilardi, S., Sharygina, N.: A new acceleration-based combination framework for array properties. In: FroCoS 15. pp. 169–185. LNCS 9322 (2015). https://doi.org/10.1007/978-3-319-24246-0 11

work page doi:10.1007/978-3-319-24246-0 2015
[4]

PURRS: Towards Computer Algebra Support for Fully Automatic Worst-Case Complexity Analysis

Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.:PURRS: Towards com- puter algebra support for fully automatic worst-case complexity analysis. CoRR abs/cs/0512056(2005). https://doi.org/10.48550/arXiv.cs/0512056

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.cs/0512056 2005
[5]

Bardin, S., Finkel, A., Leroux, J., Petrucci, L.:FAST: Acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf.10(5), 401–424 (2008). https: //doi.org/10.1007/s10009-008-0064-3

work page doi:10.1007/s10009-008-0064-3 2008
[6]

Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016), https://smt-lib.org/

work page 2016
[7]

In: TACAS ’25

Beyer, D., Strejˇ cek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: TACAS ’25. pp. 151–186. LNCS 15698 (2025). https://doi.org/ 10.1007/978-3-031-90660-2 9, website of SV-COMP: https://sv-comp.sosy-lab.org

work page doi:10.1007/978-3-031-90660-2 2025
[9]

Boigelot, B.: On iterating linear transformations over recognizable sets of inte- gers. Theor. Comput. Sci.309(1-3), 413–468 (2003). https://doi.org/10.1016/ S0304-3975(03)00314-1

work page 2003
[10]

In: TACAS ’09

Bozga, M., Gˆ ırlea, C., Iosif, R.: Iterating octagons. In: TACAS ’09. pp. 337–351. LNCS 5505 (2009). https://doi.org/10.1007/978-3-642-00768-2 29

work page doi:10.1007/978-3-642-00768-2 2009
[11]

In: CAV ’10

Bozga, M., Iosif, R., Koneˇ cn´ y, F.: Fast acceleration of ultimately periodic re- lations. In: CAV ’10. pp. 227–242. LNCS 6174 (2010). https://doi.org/10.1007/ 978-3-642-14295-6 23

work page 2010
[12]

Bozga, M., Iosif, R., Koneˇ cn´ y, F.: Relational analysis of integer programs. Tech. Rep. TR-2012-10, VERIMAG (2012), https://www-verimag.imag.fr/TR/TR-2012-10. pdf

work page 2012
[13]

Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: VMCAI ’06. pp. 427–442. LNCS 3855 (2006). https://doi.org/10.1007/11609773 28

work page doi:10.1007/11609773 2006
[14]

Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. J. Satisf. Boolean Model. Comput.6(1-3), 165–201 (2009). https://doi.org/10.3233/ SAT190067

work page 2009
[15]

CHC Competition Input Format, https://chc-comp.github.io/format.html

work page
[16]

In: CAV ’98

Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and Presburger arithmetic. In: CAV ’98. pp. 268–279. LNCS 1427 (1998). https://doi.org/10.1007/ BFb0028751 Accelerating Loops with Arrays 17

work page 1998
[17]

In: VMCAI ’22

Ernst, G.: Loop verification with invariants and contracts. In: VMCAI ’22. pp. 69–92. LNCS 13182 (2022). https://doi.org/10.1007/978-3-030-94583-1 4

work page doi:10.1007/978-3-030-94583-1 2022
[18]

Frohn, F.:LoATwebsite (2018), https://loat-developers.github.io/LoAT/

work page 2018
[19]

In: TACAS ’20

Frohn, F.: A calculus for modular loop acceleration. In: TACAS ’20. pp. 58–76. LNCS 12078 (2020). https://doi.org/10.1007/978-3-030-45190-5 4

work page doi:10.1007/978-3-030-45190-5 2020
[20]

In: IJCAR ’22

Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with LoAT(system description). In: IJCAR ’22. pp. 712–722. LNCS 13385 (2022). https://doi.org/10.1007/978-3-031-10769-6 41

work page doi:10.1007/978-3-031-10769-6 2022
[21]

In: SAS ’23

Frohn, F., Giesl, J.: ADCL: Acceleration Driven Clause Learning for constrained Horn clauses. In: SAS ’23. pp. 259–285. LNCS 14284 (2023). https://doi.org/10. 1007/978-3-031-44245-2 13

work page 2023
[22]

In: IJCAR ’24

Frohn, F., Giesl, J.: Satisfiability modulo exponential integer arithmetic. In: IJCAR ’24. pp. 344–365. LNCS 14739 (2024). https://doi.org/10.1007/ 978-3-031-63498-7 21

work page 2024
[23]

In: FM ’24

Frohn, F., Giesl, J.: Integrating loop acceleration into bounded model checking. In: FM ’24. pp. 73–91. LNCS 14933 (2024). https://doi.org/10.1007/978-3-031-71162-6 4

work page doi:10.1007/978-3-031-71162-6 2024
[24]

Frohn, F.:HornKlaus(2026), https://github.com/LoAT-developers/HornKlaus

work page 2026
[25]

Accelerating Loops with Arrays

Frohn, F., Giesl, J.: Evaluation of “Accelerating Loops with Arrays” (2026), https: //loat-developers.github.io/arrays-eval/

work page 2026
[26]

3.0 - User Manual (2020), http://users.mat.unimi.it/users/ ghilardi/mcmt/UM MCMT 3.0.pdf

Ghilardi, S.:MCMTv. 3.0 - User Manual (2020), http://users.mat.unimi.it/users/ ghilardi/mcmt/UM MCMT 3.0.pdf

work page 2020
[27]

In: CAV ’15

Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: TheSeaHornverification framework. In: CAV ’15. pp. 343–361. LNCS 9206 (2015). https://doi.org/10.1007/ 978-3-319-21690-4 20

work page 2015
[28]

In: LPAR 10

Henzinger, T.A., Hottelier, T., Kov´ acs, L., Rybalchenko, A.:Aligatorsfor arrays (tool paper). In: LPAR 10. pp. 348–356. LNCS 6397 (2010). https://doi.org/10. 1007/978-3-642-16242-8 25

work page 2010
[29]

Herrmann, R., R¨ ummer, P.: What’s decidable about arrays with sums? In: CADE ’25. pp. 56–74. LNCS 15943 (2025). https://doi.org/10.1007/978-3-031-99984-0 4

work page doi:10.1007/978-3-031-99984-0 2025
[30]

In: FMCAD ’18

Hojjat, H., R¨ ummer, P.: TheEldaricaHorn solver. In: FMCAD ’18. pp. 1–7 (2018). https://doi.org/10.23919/FMCAD.2018.8603013

work page doi:10.23919/fmcad.2018.8603013 2018
[31]

In: TACAS ’16

Koneˇ cn´ y, F.: PTIME computation of transitive closures of octagonal rela- tions. In: TACAS ’16. pp. 645–661. LNCS 9636 (2016). https://doi.org/10.1007/ 978-3-662-49674-9 42

work page 2016
[33]

In: FASE ’09

Kov´ acs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: FASE ’09. pp. 470–485. LNCS 5503 (2009). https://doi.org/10. 1007/978-3-642-00593-0 33

work page 2009
[34]

Formal Methods Syst

Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops inC programs for fast counterexample detection. Formal Methods Syst. Des.47(1), 75–92 (2015). https://doi.org/10.1007/s10703-015-0228-1

work page doi:10.1007/s10703-015-0228-1 2015
[35]

In: Program Ver- ification - Fundamental Issues in Computer Science, Studies in Cognitive Sys- tems, vol

McCarthy, J.: Towards a mathematical science of computation. In: Program Ver- ification - Fundamental Issues in Computer Science, Studies in Cognitive Sys- tems, vol. 14, pp. 35–56. Springer Netherlands (1993). https://doi.org/10.1007/ 978-94-011-1793-7 2

work page 1993
[36]

In: CA V ’23

Niemetz, A., Preiner, M.:Bitwuzla. In: CAV ’23. pp. 3–17. LNCS 13965 (2023). https://doi.org/10.1007/978-3-031-37703-7 1

work page doi:10.1007/978-3-031-37703-7 2023
[37]

In: TACAS ’08

de Moura, L., Bjørner, N.:Z3: An efficient SMT solver. In: TACAS ’08. pp. 337–340. LNCS 4963 (2008). https://doi.org/10.1007/978-3-540-78800-3 24 18 F. Frohn, J. Giesl

work page doi:10.1007/978-3-540-78800-3 2008
[38]

In: Proc

Preiner, M., Niemetz, A., Biere, A.: Lemmas on demand for lambdas. In: Proc. 2nd Int. Workshop on Design and Implementation of Formal Tools and Systems. CEUR Workshop Proceedings 1130 (2013), https://ceur-ws.org/Vol-1130/paper 7.pdf

work page 2013
[39]

substitutions

Preiner, M.: Lambdas, Arrays and Quantifiers. Ph.D. thesis, Johannes Kepler Universit¨ at Linz (2017), https://epub.jku.at/obvulihs/content/titleinfo/1915381 A Reasoning about Lambdas Using the approach from Sect. 5, we obtain quantifier-free closed forms for arrays, which allows us to encode many verification problems as SMT problems. Example 29 (Encodin...

work page arXiv 2017

[1] [1]

In: FroCoS 13

Alberti, F., Ghilardi, S., Sharygina, N.: Definability of accelerated relations in a theory of arrays and its applications. In: FroCoS 13. pp. 23–39. LNCS 8152 (2013). https://doi.org/10.1007/978-3-642-40885-4 3

work page doi:10.1007/978-3-642-40885-4 2013

[2] [2]

Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. J. Autom. Reason.54(4), 327–352 (2015). https://doi.org/10.1007/ S10817-015-9323-7

work page 2015

[3] [3]

In: FroCoS 15

Alberti, F., Ghilardi, S., Sharygina, N.: A new acceleration-based combination framework for array properties. In: FroCoS 15. pp. 169–185. LNCS 9322 (2015). https://doi.org/10.1007/978-3-319-24246-0 11

work page doi:10.1007/978-3-319-24246-0 2015

[4] [4]

PURRS: Towards Computer Algebra Support for Fully Automatic Worst-Case Complexity Analysis

Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.:PURRS: Towards com- puter algebra support for fully automatic worst-case complexity analysis. CoRR abs/cs/0512056(2005). https://doi.org/10.48550/arXiv.cs/0512056

work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.cs/0512056 2005

[5] [5]

Bardin, S., Finkel, A., Leroux, J., Petrucci, L.:FAST: Acceleration from theory to practice. Int. J. Softw. Tools Technol. Transf.10(5), 401–424 (2008). https: //doi.org/10.1007/s10009-008-0064-3

work page doi:10.1007/s10009-008-0064-3 2008

[6] [6]

Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016), https://smt-lib.org/

work page 2016

[7] [7]

In: TACAS ’25

Beyer, D., Strejˇ cek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: TACAS ’25. pp. 151–186. LNCS 15698 (2025). https://doi.org/ 10.1007/978-3-031-90660-2 9, website of SV-COMP: https://sv-comp.sosy-lab.org

work page doi:10.1007/978-3-031-90660-2 2025

[8] [9]

Boigelot, B.: On iterating linear transformations over recognizable sets of inte- gers. Theor. Comput. Sci.309(1-3), 413–468 (2003). https://doi.org/10.1016/ S0304-3975(03)00314-1

work page 2003

[9] [10]

In: TACAS ’09

Bozga, M., Gˆ ırlea, C., Iosif, R.: Iterating octagons. In: TACAS ’09. pp. 337–351. LNCS 5505 (2009). https://doi.org/10.1007/978-3-642-00768-2 29

work page doi:10.1007/978-3-642-00768-2 2009

[10] [11]

In: CAV ’10

Bozga, M., Iosif, R., Koneˇ cn´ y, F.: Fast acceleration of ultimately periodic re- lations. In: CAV ’10. pp. 227–242. LNCS 6174 (2010). https://doi.org/10.1007/ 978-3-642-14295-6 23

work page 2010

[11] [12]

Bozga, M., Iosif, R., Koneˇ cn´ y, F.: Relational analysis of integer programs. Tech. Rep. TR-2012-10, VERIMAG (2012), https://www-verimag.imag.fr/TR/TR-2012-10. pdf

work page 2012

[12] [13]

Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: VMCAI ’06. pp. 427–442. LNCS 3855 (2006). https://doi.org/10.1007/11609773 28

work page doi:10.1007/11609773 2006

[13] [14]

Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. J. Satisf. Boolean Model. Comput.6(1-3), 165–201 (2009). https://doi.org/10.3233/ SAT190067

work page 2009

[14] [15]

CHC Competition Input Format, https://chc-comp.github.io/format.html

work page

[15] [16]

In: CAV ’98

Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and Presburger arithmetic. In: CAV ’98. pp. 268–279. LNCS 1427 (1998). https://doi.org/10.1007/ BFb0028751 Accelerating Loops with Arrays 17

work page 1998

[16] [17]

In: VMCAI ’22

Ernst, G.: Loop verification with invariants and contracts. In: VMCAI ’22. pp. 69–92. LNCS 13182 (2022). https://doi.org/10.1007/978-3-030-94583-1 4

work page doi:10.1007/978-3-030-94583-1 2022

[17] [18]

Frohn, F.:LoATwebsite (2018), https://loat-developers.github.io/LoAT/

work page 2018

[18] [19]

In: TACAS ’20

Frohn, F.: A calculus for modular loop acceleration. In: TACAS ’20. pp. 58–76. LNCS 12078 (2020). https://doi.org/10.1007/978-3-030-45190-5 4

work page doi:10.1007/978-3-030-45190-5 2020

[19] [20]

In: IJCAR ’22

Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with LoAT(system description). In: IJCAR ’22. pp. 712–722. LNCS 13385 (2022). https://doi.org/10.1007/978-3-031-10769-6 41

work page doi:10.1007/978-3-031-10769-6 2022

[20] [21]

In: SAS ’23

Frohn, F., Giesl, J.: ADCL: Acceleration Driven Clause Learning for constrained Horn clauses. In: SAS ’23. pp. 259–285. LNCS 14284 (2023). https://doi.org/10. 1007/978-3-031-44245-2 13

work page 2023

[21] [22]

In: IJCAR ’24

Frohn, F., Giesl, J.: Satisfiability modulo exponential integer arithmetic. In: IJCAR ’24. pp. 344–365. LNCS 14739 (2024). https://doi.org/10.1007/ 978-3-031-63498-7 21

work page 2024

[22] [23]

In: FM ’24

Frohn, F., Giesl, J.: Integrating loop acceleration into bounded model checking. In: FM ’24. pp. 73–91. LNCS 14933 (2024). https://doi.org/10.1007/978-3-031-71162-6 4

work page doi:10.1007/978-3-031-71162-6 2024

[23] [24]

Frohn, F.:HornKlaus(2026), https://github.com/LoAT-developers/HornKlaus

work page 2026

[24] [25]

Accelerating Loops with Arrays

Frohn, F., Giesl, J.: Evaluation of “Accelerating Loops with Arrays” (2026), https: //loat-developers.github.io/arrays-eval/

work page 2026

[25] [26]

3.0 - User Manual (2020), http://users.mat.unimi.it/users/ ghilardi/mcmt/UM MCMT 3.0.pdf

Ghilardi, S.:MCMTv. 3.0 - User Manual (2020), http://users.mat.unimi.it/users/ ghilardi/mcmt/UM MCMT 3.0.pdf

work page 2020

[26] [27]

In: CAV ’15

Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: TheSeaHornverification framework. In: CAV ’15. pp. 343–361. LNCS 9206 (2015). https://doi.org/10.1007/ 978-3-319-21690-4 20

work page 2015

[27] [28]

In: LPAR 10

Henzinger, T.A., Hottelier, T., Kov´ acs, L., Rybalchenko, A.:Aligatorsfor arrays (tool paper). In: LPAR 10. pp. 348–356. LNCS 6397 (2010). https://doi.org/10. 1007/978-3-642-16242-8 25

work page 2010

[28] [29]

Herrmann, R., R¨ ummer, P.: What’s decidable about arrays with sums? In: CADE ’25. pp. 56–74. LNCS 15943 (2025). https://doi.org/10.1007/978-3-031-99984-0 4

work page doi:10.1007/978-3-031-99984-0 2025

[29] [30]

In: FMCAD ’18

Hojjat, H., R¨ ummer, P.: TheEldaricaHorn solver. In: FMCAD ’18. pp. 1–7 (2018). https://doi.org/10.23919/FMCAD.2018.8603013

work page doi:10.23919/fmcad.2018.8603013 2018

[30] [31]

In: TACAS ’16

Koneˇ cn´ y, F.: PTIME computation of transitive closures of octagonal rela- tions. In: TACAS ’16. pp. 645–661. LNCS 9636 (2016). https://doi.org/10.1007/ 978-3-662-49674-9 42

work page 2016

[31] [33]

In: FASE ’09

Kov´ acs, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: FASE ’09. pp. 470–485. LNCS 5503 (2009). https://doi.org/10. 1007/978-3-642-00593-0 33

work page 2009

[32] [34]

Formal Methods Syst

Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops inC programs for fast counterexample detection. Formal Methods Syst. Des.47(1), 75–92 (2015). https://doi.org/10.1007/s10703-015-0228-1

work page doi:10.1007/s10703-015-0228-1 2015

[33] [35]

In: Program Ver- ification - Fundamental Issues in Computer Science, Studies in Cognitive Sys- tems, vol

McCarthy, J.: Towards a mathematical science of computation. In: Program Ver- ification - Fundamental Issues in Computer Science, Studies in Cognitive Sys- tems, vol. 14, pp. 35–56. Springer Netherlands (1993). https://doi.org/10.1007/ 978-94-011-1793-7 2

work page 1993

[34] [36]

In: CA V ’23

Niemetz, A., Preiner, M.:Bitwuzla. In: CAV ’23. pp. 3–17. LNCS 13965 (2023). https://doi.org/10.1007/978-3-031-37703-7 1

work page doi:10.1007/978-3-031-37703-7 2023

[35] [37]

In: TACAS ’08

de Moura, L., Bjørner, N.:Z3: An efficient SMT solver. In: TACAS ’08. pp. 337–340. LNCS 4963 (2008). https://doi.org/10.1007/978-3-540-78800-3 24 18 F. Frohn, J. Giesl

work page doi:10.1007/978-3-540-78800-3 2008

[36] [38]

In: Proc

Preiner, M., Niemetz, A., Biere, A.: Lemmas on demand for lambdas. In: Proc. 2nd Int. Workshop on Design and Implementation of Formal Tools and Systems. CEUR Workshop Proceedings 1130 (2013), https://ceur-ws.org/Vol-1130/paper 7.pdf

work page 2013

[37] [39]

substitutions

Preiner, M.: Lambdas, Arrays and Quantifiers. Ph.D. thesis, Johannes Kepler Universit¨ at Linz (2017), https://epub.jku.at/obvulihs/content/titleinfo/1915381 A Reasoning about Lambdas Using the approach from Sect. 5, we obtain quantifier-free closed forms for arrays, which allows us to encode many verification problems as SMT problems. Example 29 (Encodin...

work page arXiv 2017