[Zurück]

L. Kovacs, A. Kovacs:
"Aligator: Experiments and Limitations";
Vortrag: 22nd International DAAAM Symposium: "Intelligent Manufactoring and Symposium: Power of Knowledge and Creativity", Vienna, Austria; 23.11.2011 - 26.11.2011; in: "Proc. of the 22nd International DAAAM Symposium: "Intelligent Manufactoring and Automation: Power of Knowledge and Creativity"", DAAAM International, Volume 22, No. 1 (2011), ISBN: 978-3-901509-83-4; S. 1145 - 1146.

We address the problem of loop invariant generation of programs over scalars and unbounded data structures. Our approach to invariant generation is implemented in the Aligator software tool. We investigate various loop classes for using Aligator and presents experimental evaluation of our method. We also discuss limitations of the approach and underline the basic principles of how and when Aligator can be successfully applied.

We address the problem of loop invariant generation of programs over scalars and unbounded data structures. Our approach to invariant generation is implemented in the Aligator software tool. We investigate various loop classes for using Aligator and presents experimental evaluation of our method. We also discuss limitations of the approach and underline the basic principles of how and when Aligator can be successfully applied.

program verification, loop invariants, polynomial relations, quantified first-order formulas

http://publik.tuwien.ac.at/files/PubDat_205761.pdf