2026-07-18T12:14:56Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:511 2024-03-06T11:06:33Z ddc:004 open_access

Automatically Generating Loop Invariants Using Quantifier Elimination Kapur, Deepak Program verification loop invariants inductive assertions quantifier elimination An approach for automatically generating loop invariants using quantifier-elimination is proposed. An invariant of a loop is hypothesized as a parameterized formula. Parameters in the invariant are discovered by generating constraints on the parameters by ensuring that the formula is indeed preserved by the execution path corresponding to every basic cycle of the loop. The parameterized formula can be successively refined by considering execution paths one by one; heuristics can be developed for determining the order in which the paths are considered. Initialization of program variables as well as the precondition and postcondition of the loop, if available, can also be used to further refine the hypothesized invariant. Constraints on parameters generated in this way are solved for possible values of parameters. If no solution is possible, this means that an invariant of the hypothesized form does not exist for the loop. Otherwise, if the parametric constraints are solvable, then under certain conditions on methods for generating these constraints, the strongest possible invariant of the hypothesized form can be generated from most general solutions of the parametric constraints. The approach is illustrated using the first-order theory of polynomial equations as well as Presburger arithmetic. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Deepak Kapur 2006 Is Part Of Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.05431.3 urn:nbn:de:0030-drops-5116 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.3 eng https://creativecommons.org/licenses/by/4.0/legalcode