zbMATH — the first resource for mathematics

Invariant generation for P-solvable loops with assignments. (English) Zbl 1142.68619
Hirsch, Edward A. (ed.) et al., Computer science – theory and applications. Third international computer science symposium in Russia, CSR 2008 Moscow, Russia, June 7–12, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-79708-1/pbk). Lecture Notes in Computer Science 5010, 349-359 (2008).
Summary: 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.
For the entire collection see [Zbl 1136.68005].
68W30 Symbolic computation and algebraic computation
PDF BibTeX Cite
Full Text: DOI