
TL;DR
This paper introduces a new loop acceleration technique for array-based loops, enabling better automated reasoning by handling complex loops with inductive lvalues and using lambda-based SMT solving.
Contribution
It presents a novel acceleration method using inductive lvalues and lambda calculus, unifying array and scalar loop acceleration for improved SMT solving.
Findings
Empirical evaluation demonstrates the effectiveness of the approach.
The technique handles loops where previous methods fail.
SMT problems are efficiently solved via lemmas on demand.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
