Talks and Poster Presentations (with Proceedings-Entry):
F. Zuleger, M. Sinn, S. Gulwani, H. Veith:
"Bound Analysis of Imperative Programs with the Size-change Abstraction";
Talk: International Static Analysis Symposium,
Venice, Italy;
2011-09-14
- 2011-09-16; in: "Lecture Notes in Computer Science",
E. Yahav (ed.);
Springer,
6887
(2011),
ISBN: 978-3-642-23701-0;
280
- 297.
English abstract:
The size-change abstraction (SCA) is an important program
abstraction for termination analysis, which has been successfully implemented in many tools for functional and logic programs. In this paper, we demonstrate that SCA is also a highly effective abstract domain for the bound analysis of imperative programs.
We have implemented a bound analysis tool based on SCA for imperative
programs. We abstract programs in a pathwise and context dependent
manner, which enables our tool to analyze real-world programs
effectively. Our work shows that SCA captures many of the essential
ideas of previous termination and bound analysis and goes beyond in a
conceptually simpler framework.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-642-23702-7_22
Related Projects:
Project Head Helmut Veith:
Proof Seeding for Software Verification
Project Head Georg Weissenbacher:
Rise-TOOLS
Created from the Publication Database of the Vienna University of Technology.