Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
F. Zuleger, M. Sinn, S. Gulwani, H. Veith:
"Bound Analysis of Imperative Programs with the Size-change Abstraction";
Vortrag: International Static Analysis Symposium,
Venice, Italy;
14.09.2011
- 16.09.2011; in: "Lecture Notes in Computer Science",
E. Yahav (Hrg.);
Springer,
6887
(2011),
ISBN: 978-3-642-23701-0;
S. 280
- 297.
Kurzfassung englisch:
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.
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-642-23702-7_22
Zugeordnete Projekte:
Projektleitung Helmut Veith:
Proof Seeding for Software Verification
Projektleitung Georg Weissenbacher:
Rise-TOOLS
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.