E-Book Overview
The book constitutes the refereed proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2005, held in Paris, France in January 2005. The 27 revised full papers presented together with an invited paper were carefully reviewed and selected from 92 submissions. The papers are organized in topical sections on numerical abstraction, verification, heap and shape analysis, abstract model checking, model checking, applied abstract interpretation, and bounded model checking.
E-Book Content
Lecture Notes in Computer Science Commenced Publication in 1973 Founding and Former Series Editors: Gerhard Goos, Juris Hartmanis, and Jan van Leeuwen Editorial Board David Hutchison Lancaster University, UK Takeo Kanade Carnegie Mellon University, Pittsburgh, PA, USA Josef Kittler University of Surrey, Guildford, UK Jon M. Kleinberg Cornell University, Ithaca, NY, USA Friedemann Mattern ETH Zurich, Switzerland John C. Mitchell Stanford University, CA, USA Moni Naor Weizmann Institute of Science, Rehovot, Israel Oscar Nierstrasz University of Bern, Switzerland C. Pandu Rangan Indian Institute of Technology, Madras, India Bernhard Steffen University of Dortmund, Germany Madhu Sudan Massachusetts Institute of Technology, MA, USA Demetri Terzopoulos New York University, NY, USA Doug Tygar University of California, Berkeley, CA, USA Moshe Y. Vardi Rice University, Houston, TX, USA Gerhard Weikum Max-Planck Institute of Computer Science, Saarbruecken, Germany 3385 This page intentionally left blank Radhia Cousot (Ed.) Verification, Model Checking, and Abstract Interpretation 6th International Conference, VMCAI 2005 Paris, France, January 17-19, 2005 Proceedings Springer eBook ISBN: Print ISBN: 3-540-30579-3 3-540-24297-X ©2005 Springer Science + Business Media, Inc. Print ©2005 Springer-Verlag Berlin Heidelberg All rights reserved No part of this eBook may be reproduced or transmitted in any form or by any means, electronic, mechanical, recording, or otherwise, without written consent from the Publisher Created in the United States of America Visit Springer's eBookstore at: and the Springer Global Website Online at: http://ebooks.springerlink.com http://www.springeronline.com Preface This volume contains the papers accepted for presentation at the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2005), which was held January 17–19, 2005 in Paris, France. VMCAI provides a forum for researchers from the communities of verification, model checking, and abstract interpretation, facilitating interaction, crossfertilization, and advancement of hybrid methods that combine the three areas. With the growing need for formal methods to reason about complex, infinitestate, and embedded systems, such hybrid methods are bound to be of great importance. VMCAI 2005 received 92 submissions. Each paper was carefully reviewed, being judged according to scientific quality, originality, and relevance to the symposium topics. Following online discussions, the program committee met in Paris, France, at the École Normale Supérieure on October 30, 2004, and selected 27 papers. In addition to the contributed papers, this volume includes contributions by outstanding invited speakers: Patrick Cousot (École Normale Supérieure, Paris), Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming; C.A.R. Hoare (Microsoft Research, Cambridge), The Verifying Compiler, a Grand Challenge for Computing Research; Amir Pnueli (New York University and Weizmann Institute of Science), Abstraction for Liveness. The VMCAI 2005 program included an invited tutorial by Sriram K. Rajamam (Microsoft Research, Redmond) on Mode