License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.05431.3
URN: urn:nbn:de:0030-drops-5116
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/511/
Go to the corresponding Portal

Kapur, Deepak

Automatically Generating Loop Invariants Using Quantifier Elimination

pdf-format:
05431.KapurDeepak.Paper.511.pdf (0.3 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{kapur:DagSemProc.05431.3,
  author =	{Kapur, Deepak},
  title =	{{Automatically Generating Loop Invariants Using Quantifier Elimination}},
  booktitle =	{Deduction and Applications},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/511},
  URN =		{urn:nbn:de:0030-drops-5116},
  doi =		{10.4230/DagSemProc.05431.3},
  annote =	{Keywords: Program verification, loop invariants, inductive assertions, quantifier elimination}
}

Keywords: Program verification, loop invariants, inductive assertions, quantifier elimination
Collection: 05431 - Deduction and Applications
Issue Date: 2006
Date of publication: 25.04.2006

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI