Talks and Poster Presentations (with Proceedings-Entry):
L. Kovacs, A. Kovacs:
"Aligator: Experiments and Limitations";
Talk: 22nd International DAAAM Symposium: "Intelligent Manufactoring and Symposium: Power of Knowledge and Creativity",
Vienna, Austria;
11-23-2011
- 11-26-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;
1145
- 1146.
English abstract:
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.
German abstract:
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.
Keywords:
program verification, loop invariants, polynomial relations, quantified first-order formulas
Electronic version of the publication:
http://publik.tuwien.ac.at/files/PubDat_205761.pdf
Created from the Publication Database of the Vienna University of Technology.