This book constitutes the refereed proceedings of the 12th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2003, held in L'Aquila, Italy in October 2003.
The 24 revised full papers and 8 short papers presented were carefully reviewed and selected from 65 submissions. The papers are organized in topical sections on software verification, automata based methods, processor verification, specification methods, theorem proving, bounded model checking, and model checking and applications.
Lecture Notes in Computer Science Edited by G. Goos, J. Hartmanis, and J. van Leeuwen
2860
3
Berlin Heidelberg New York Hong Kong London Milan Paris Tokyo
Daniel Geist Enrico Tronci (Eds.)
Correct Hardware Design and Verification Methods 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003 L’Aquila, Italy, October 21-24, 2003 Proceedings
13
Series Editors Gerhard Goos, Karlsruhe University, Germany Juris Hartmanis, Cornell University, NY, USA Jan van Leeuwen, Utrecht University, The Netherlands Volume Editors Daniel Geist Haifa University, IBM Haifa Research Lab Mount Carmel, Haifa, Israel E-mail:
[email protected] Enrico Tronci University of Rome "La Sapienza", Computer Science Department Via Salaria 113, 00198 Rome, Italy E-mail:
[email protected]
Cataloging-in-Publication Data applied for A catalog record for this book is available from the Library of Congress Bibliographic information published by Die Deutsche Bibliothek Die Deutsche Bibliothek lists this publication in the Deutsche Nationalbibliographie; detailed bibliographic data is available in the Internet at .
CR Subject Classification (1998): F.3.1, B, D.2.4, F.4.1, I.2.3, J.6 ISSN 0302-9743 ISBN 3-540-20363-X Springer-Verlag Berlin Heidelberg New York This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting, reproduction on microfilms or in any other way, and storage in data banks. Duplication of this publication or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965, in its current version, and permission for use must always be obtained from Springer-Verlag. Violations are liable for prosecution under the German Copyright Law. Springer-Verlag Berlin Heidelberg New York a member of BertelsmannSpringer Science+Business Media GmbH http://www.springer.de ©2003 IFIP International Federation for Information Processing, Hofstrasse 3, A-2361 Laxenburg,Austria Printed in Germany Typesetting: Camera-ready by author, data conversion by PTP-Berlin GmbH Printed on acid-free paper SPIN: 10966464 06/3142 543210
Preface
This volume contains the proceedings of CHARME 2003, the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods. CHARME 2003 continues the series of working conferences devoted to the development and use of leading-edge formal techniques and tools for the design and verification of hardware and hardware-like systems. Previous events in the ‘CHARME’ series were held in Edinburgh (2001), Bad Herrenalb (1999), Montreal (1997), Frankfurt (1995), Arles (1993) and Turin (1991). This series of meetings were organized in cooperation with IFIP WG 10.5 and 10.2. Prior meetings, stretching back to the earliest days of formal hardware verification were held under various names in Miami (1990), Leuven (1989), Glasgow