Document Open Access Logo

Linear Loop Synthesis for Quadratic Invariants

Authors S. Hitarth , George Kenison , Laura Kovács , Anton Varonka

PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

S. Hitarth
  • Hong Kong University of Science and Technology, Hong Kong
George Kenison
  • Liverpool John Moores University, UK
Laura Kovács
  • TU Wien, Austria
Anton Varonka
  • TU Wien, Austria

Funding

The project leading to this publication has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 101034440. The project was also partially supported by the ERC consolidator grant ARTIST 101002685 and by the Vienna Science and Technology Fund (WWTF) [10.47379/ICT19018].

Cite AsGet BibTex

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
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. T. Andreescu and D. Andrica. Quadratic Diophantine Equations. Developments in Mathematics. Springer New York, 2016. Google Scholar
  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. Google Scholar
  3. Zenon I. Borevich and Igor R. Shafarevich. Number Theory. Pure and Applied Mathematics. Academic Press, New York, NY, 1966. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  23. Seymour Lipschutz and Marc Lipson. Schaum’s Outline of Linear Algebra. Schaum’s Outline Series. McGraw-Hill, New York, fourth edition, 2009. Google Scholar
  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. Google Scholar
  26. A. Meyer. Mathematische Mittheilungen. Vierteljahrsschrift der Naturforschenden Gesellschaft in Zürich, 29:209-222, 1884. Google Scholar
  27. Ivan Niven. Irrational numbers. Mathematical Association of America; distributed by John Wiley & Sons, Inc., New York, N.Y.,,, 1956. Google Scholar
  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. Google Scholar
  30. Carl Ludwig Siegel. Zur theorie der quadratischen formen. Nachrichten der Akademie der Wissenschaften in Göttingen, Mathematisch-Physikalische Klasse, 3:21-46, 1972. Google Scholar
  31. Joseph H. Silverman and John T. Tate. Rational Points on Elliptic Curves. Springer Publishing Company, Incorporated, 2nd edition, 2015. Google Scholar
  32. Denis Simon. Quadratic equations in dimensions 4, 5 and more. 2005. Google Scholar
  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. Google Scholar
  35. Sergei Treil. Linear algebra done wrong, 2004. Google Scholar
  36. Leonid Vaserstein. Polynomial parametrization for the solutions of diophantine equations and arithmetic groups. Annals of Mathematics, 171:979-1009, 2010. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact