Invariant generation for P-solvable loops with assignments

We discuss interesting properties of a general technique for inferring polynomial invariants for a subfamily of imperative loops, called the P-solvable loops, with assignments only. The approach combines algorithmic combinatorics, polynomial algebra and computational logic, and it is implemented in a new software package called Aligator. We present a collection of examples illustrating the power of the framework.


Published in:
Computer Science - Theory And Applications, 5010, 349-359
Presented at:
3rd International Computer Science Symposium, Moscow, RUSSIA, Jun 07-12, 2008
Year:
2008
Publisher:
Springer-Verlag New York, Ms Ingrid Cunningham, 175 Fifth Ave, New York, Ny 10010 Usa
ISBN:
978-3-540-79708-1
Keywords:
Laboratories:




 Record created 2010-11-30, last modified 2018-01-28


Rate this document:

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