Reasoning algebraically about P-solvable loops

We present a method for generating polynomial invariants for a subfamily of imperative loops operating on numbers, called the P-solvable loops. The method uses algorithmic combinatorics and algebraic techniques. The approach is shown to be complete for some special cases. By completeness we mean that it generates a set of polynomial invariants from which, under additional assumptions, any polynomial invariant can be derived. These techniques are implemented in a new software package Aligator written in Mathematica and successfully tried on many programs implementing interesting algorithms working on numbers.


Published in:
Tools And Algorithms For The Construction And Analysis Of Systems, 4963, 249-264
Presented at:
14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Budapest, HUNGARY, Mar 29-Apr 06, 2008
Year:
2008
Publisher:
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa
ISBN:
978-3-540-78799-0
Keywords:
Laboratories:




 Record created 2010-11-30, last modified 2018-09-25


Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)