Document

# Linear Loop Synthesis for Quadratic Invariants

## File

LIPIcs.STACS.2024.41.pdf
• Filesize: 0.93 MB
• 18 pages

## Cite As

S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka. Linear Loop Synthesis for Quadratic Invariants. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 41:1-41:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.STACS.2024.41

## Abstract

Invariants are key to formal loop verification as they capture loop properties that are valid before and after each loop iteration. Yet, generating invariants is a notorious task already for syntactically restricted classes of loops. Rather than generating invariants for given loops, in this paper we synthesise loops that exhibit a predefined behaviour given by an invariant. From the perspective of formal loop verification, the synthesised loops are thus correct by design and no longer need to be verified. To overcome the hardness of reasoning with arbitrarily strong invariants, in this paper we construct simple (non-nested) while loops with linear updates that exhibit polynomial equality invariants. Rather than solving arbitrary polynomial equations, we consider loop properties defined by a single quadratic invariant in any number of variables. We present a procedure that, given a quadratic equation, decides whether a loop with affine updates satisfying this equation exists. Furthermore, if the answer is positive, the procedure synthesises a loop and ensures its variables achieve infinitely many different values.

## Subject Classification

##### ACM Subject Classification
• Mathematics of computing → Discrete mathematics
• Computing methodologies → Equation and inequality solving algorithms
• Computing methodologies → Algebraic algorithms
##### Keywords
• program synthesis
• loop invariants
• verification
• Diophantine equations

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. T. Andreescu and D. Andrica. Quadratic Diophantine Equations. Developments in Mathematics. Springer New York, 2016.
2. Saugata Basu, Richard Pollack, and Marie-Françoise Roy. Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics). Springer-Verlag, Berlin, Heidelberg, 2006.
3. Zenon I. Borevich and Igor R. Shafarevich. Number Theory. Pure and Applied Mathematics. Academic Press, New York, NY, 1966.
4. J. L. Britton. Integer solutions of systems of quadratic equations. Mathematical Proceedings of the Cambridge Philosophical Society, 86(3):385-389, 1979. URL: https://doi.org/10.1017/S0305004100056218.
5. T. D. Browning and R. Dietmann. On the representation of integers by quadratic forms. Proceedings of the London Mathematical Society, 96(2):389-416, 2008. URL: https://doi.org/10.1112/plms/pdm032.
6. Pierre Castel. Solving quadratic equations in dimension 5 or more without factoring. In ANTS X - Proceedings of the Tenth Algorithmic Number Theory Symposium, volume 1 of Open Book Ser., pages 213-233. Math. Sci. Publ., Berkeley, CA, 2013. URL: https://doi.org/10.2140/obs.2013.1.213.
7. Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Ehsan Kafshdar Goharshady. Polynomial invariant generation for non-deterministic recursive programs. In PLDI 2020, pages 672-687, 2020. URL: https://doi.org/10.1145/3385412.3385969.
8. H. Cohen. Number Theory: Volume I: Tools and Diophantine Equations. Graduate Texts in Mathematics. Springer New York, 2007.
9. J. E. Cremona and D. Rusin. Efficient solution of rational conics. Math. Comp., 72(243):1417-1441, 2003. URL: https://doi.org/10.1090/S0025-5718-02-01480-1.
10. Martin Davis. On the number of solutions of diophantine equations. Proceedings of the American Mathematical Society, 35(2):552-554, 1972.
11. Emilie Dufresne, Parker B. Edwards, Heather A. Harrington, and Jonathan D. Hauenstein. Sampling real algebraic varieties for topological data analysis, 2018. URL: https://arxiv.org/abs/1802.07716.
12. G. Everest, A. van der Poorten, I. Shparlinski, and T. Ward. Recurrence sequences, volume 104 of Math. Surveys Monogr. Amer. Math. Soc., Providence, RI, 2003. URL: https://doi.org/10.1090/surv/104.
13. Amir Kafshdar Goharshady, S. Hitarth, Fatemeh Mohammadi, and Harshit Jitendra Motwani. Algebro-geometric algorithms for template-based synthesis of polynomial programs. Proc. ACM Program. Lang., 7(OOPSLA1), April 2023. URL: https://doi.org/10.1145/3586052.
14. Fritz J. Grunewald and Daniel Segal. How to solve a quadratic equation in integers. Mathematical Proceedings of the Cambridge Philosophical Society, 89(1):1-5, 1981. URL: https://doi.org/10.1017/S030500410005787X.
15. S. Hitarth, George Kenison, Laura Kovács, and Anton Varonka. Linear loop synthesis for quadratic invariants, 2023. Extended version. URL: https://arxiv.org/abs/2310.05120.
16. Ehud Hrushovski, Joël Ouaknine, Amaury Pouly, and James Worrell. On strongest algebraic program invariants. J. ACM, August 2023. Just Accepted. URL: https://doi.org/10.1145/3614319.
17. Andreas Humenberger, Daneshvar Amrollahi, Nikolaj Bjørner, and Laura Kovács. Algebra-based reasoning for loop synthesis. Form. Asp. Comput., 34(1), July 2022. URL: https://doi.org/10.1145/3527458.
18. K. Ireland and M.I. Rosen. A Classical Introduction to Modern Number Theory. Graduate Texts in Mathematics. Springer, 1990.
19. Bertrand Jeannet, Peter Schrammel, and Sriram Sankaranarayanan. Abstract acceleration of general linear loops. SIGPLAN Not., 49(1):529-540, January 2014. URL: https://doi.org/10.1145/2578855.2535843.
20. Manuel Kauers and Peter Paule. The Concrete Tetrahedron - Symbolic Sums, Recurrence Equations, Generating Functions, Asymptotic Estimates. Texts & Monographs in Symbolic Computation. Springer, 2011.
21. George Kenison, Laura Kovács, and Anton Varonka. From polynomial invariants to linear loops. In Proceedings of the 2023 International Symposium on Symbolic and Algebraic Computation, ISSAC '23, pages 398-406, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3597066.3597109.
22. Zachary Kincaid, Jason Breck, John Cyphert, and Thomas W. Reps. Closed Forms for Numerical Loops. In Proc. of POPL, pages 55:1-55:29, 2019.
23. Seymour Lipschutz and Marc Lipson. Schaum’s Outline of Linear Algebra. Schaum’s Outline Series. McGraw-Hill, New York, fourth edition, 2009.
24. D. W. Masser. How to solve a quadratic equation in rationals. Bulletin of the London Mathematical Society, 30(1):24-28, 1998. URL: https://doi.org/10.1112/S0024609397003913.
25. Yuri Matiyasevich. Enumerable sets are Diophantine. Soviet Math. Dokl., 11:354-358, 1970.
26. A. Meyer. Mathematische Mittheilungen. Vierteljahrsschrift der Naturforschenden Gesellschaft in Zürich, 29:209-222, 1884.
27. Ivan Niven. Irrational numbers. Mathematical Association of America; distributed by John Wiley & Sons, Inc., New York, N.Y.,,, 1956.
28. Joël Ouaknine and James Worrell. On linear recurrence sequences and loop termination. ACM SIGLOG News, 2(2):4-13, April 2015. URL: https://doi.org/10.1145/2766189.2766191.
29. Alexandra Shlapentokh. Defining integers. The Bulletin of Symbolic Logic, 17(2):230-251, 2011.
30. Carl Ludwig Siegel. Zur theorie der quadratischen formen. Nachrichten der Akademie der Wissenschaften in Göttingen, Mathematisch-Physikalische Klasse, 3:21-46, 1972.
31. Joseph H. Silverman and John T. Tate. Rational Points on Elliptic Curves. Springer Publishing Company, Incorporated, 2nd edition, 2015.
32. Denis Simon. Quadratic equations in dimensions 4, 5 and more. 2005.
33. Denis Simon. Solving quadratic equations using reduced unimodular quadratic forms. Math. Comp., 74(251):1531-1543, 2005. URL: https://doi.org/10.1090/S0025-5718-05-01729-1.
34. T. Skolem. Diophantische Gleichungen. Ergebnisse der Mathematik und ihrer Grenzgebiete. J. Springer, 1938.
35. Sergei Treil. Linear algebra done wrong, 2004.
36. Leonid Vaserstein. Polynomial parametrization for the solutions of diophantine equations and arithmetic groups. Annals of Mathematics, 171:979-1009, 2010.
X

Feedback for Dagstuhl Publishing