Infoscience

Conference paper

A Complete Invariant Generation Approach for P-solvable Loops

Kovacs, Laura
  • Presented at: 7th International Andrei Ershov Memorial Conference on Perspectives of Systems Informatics, Novosibirsk, RUSSIA, Jun 15-19, 2009
  • Published in: Perspectives Of Systems Informatics (ISBN: 978-3-642-11485-4), vol. 5947, p. 242-256
  • Series: Lecture Notes in Computer Science
  • Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa, 2010

We present an algorithm for generating all polynomial invariants of P-solvable loops with assignments and nested conditionals. We prove termination of our algorithm. The proof relies on showing that the dimensions of the prime ideals from the minimal decomposition of the ideals generated at an iteration of our algorithm either remain the same or decrease at the next iteration of the algorithm. Our experimental results report that our method takes less iterations and/or time than other polynomial invariant generation techniques.

Fulltext

  • There is no available fulltext. Please contact the lab or the authors.

Related material

Contacts