Tools
Tools
Hitarth, S, Kenison, G, Kovács, L and Varonka, A (2024) Linear Loop Synthesis for Quadratic Invariants. In: Leibniz International Proceedings in Informatics (LIPIcs) , 289. (41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024), 12th Mar - 14 Mar 2024, Clermont-Ferrand, France).
|
Text
Linear Loop Synthesis for Quadratic Invariants.pdf - Published Version Available under License Creative Commons Attribution. Download (985kB) | Preview |
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. 2012 ACM Subject Classification Mathematics of computing → Discrete mathematics; Computing methodologies → Equation and inequality solving algorithms; Computing methodologies → Algebraic algorithms
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Uncontrolled Keywords: | program synthesis; loop invariants; verification |
| Subjects: | Q Science > QA Mathematics > QA75 Electronic computers. Computer science |
| Divisions: | Computer Science and Mathematics |
| Publisher: | Schloss Dagstuhl – Leibniz-Zentrum für Informatik |
| Related URLs: | |
| SWORD Depositor: | A Symplectic |
| Date Deposited: | 16 Oct 2024 09:07 |
| Last Modified: | 16 Oct 2024 09:07 |
| DOI or ID number: | 10.4230/LIPIcs.STACS.2024.41 |
| URI: | https://researchonline.ljmu.ac.uk/id/eprint/24524 |
 |
View Item |