Fully Automatic Verification of Absence of Errors via Interprocedural Integer Analysis
Ron Ellenbogen · 2004
I would like to express my sincere gratitude to all those who contributed to the completion of my thesis. First, I would like to express my deep gratitude, respect, and thanks to Dr. Shmuel (Mooly) Sagiv, my supervisor. This thesis would have been impossible to complete without his constant encouragement, guidance, patience and support. I thank Dr. Nurit Dor for her guidance and support. Nurit’s extensive knowledge of the issues researched in this thesis, as well as her willingness to help and to share her knowledge, were a great help in the completion of this thesis. I am also grateful for the help of Prof. Roberto Bagnara in the implementation of the iCSSV tool. Without Roberto’s help concerning the correct usage of the Parma Polyhedra library and his great enthusiasm towards developing the implementation, iCSSV would not have been able to run on the programs it runs on today. To my colleagues from the Tel-Aviv Programming Languages group: Roman Manevich, Greta Yorsh, and Noam Rinetzky, for their ideas, support and cheerfulness. To Izhakian Zur and Nir Andelman for all of the over lunch discussions concerning University, research, politics and