CAV01: Accepted Papers


Regular Papers

4 Rewriting for Symbolic Execution of State Machine Models J Strother Moore
25 Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks Zhe Dang
32 Efficient Model Checking Via Buechi Tableau Automata Girish Bhat, Rance Cleaveland, Alex Groce
36 Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2^m) Sumio Morioka, Yasunao Katayama, Toshiyuki Yamane
41 Automated Inductive Verification of Parameterized Protocols Abhik Roychoudhury I.V. Ramakrishnan
42 Model Checking with formula-dependent abstract models Alexander Asteroth, Christel Baier, Ulrich A{\ss}mann
50 Verifying Network Protocol Implementations by Symbolic Refinement Checking Rajeev Alur and Bow-Yaw Wang
54 Formalizing a JVML verifier for initialization in a theorem prover Yves Bertot
57 A Fast Bisimulation Algorithm Agostino Dovier, Carla Piazza, and Alberto Policriti
58 A Unified Model Checking Approach for Safety Properties of Parameterized Systems Monika Maidl
61 A Practical Approach to Coverage in Model Checking Hana Chockler, Orna Kupferman, Robert Kurshan, Moshe Vardi
62 Meta-BDDs: a decomposed representation for layered symbolic manipulation of Boolean functions Gianpiero Cabodi
67 As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata Kim Larsen Gerd Behrmann Ed Brinksma Ansgar Fehnker Thomas Hune Paul Pettersson Judi Romijn
74 Attacking Symbolic State Explosion in Parameterized Verification Giorgio Delzanno, Jean-Francois Raskin, and Laurent Van Begin
78 A BDD-based Model Checker for Recursive Programs Javier Esparza, Stefan Schwoon
80 Microarchitecture Verification by Compositional Model Checking R. Jhala and K. L. McMillan
87 Analysis of Recursive State Machines R. Alur, K. Etessami, and M. Yannakakis
88 Benefits of Bounded Model Checking at an Industrial Setting Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, Moshe Y. Vardi
93 CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination John Moondanos Carl Seger Ziyad Hanna Daher Kaiss
98 Automatic Abstraction for Verification of Timed Circuits and Systems Hao Zheng, Eric Mercer, Chris Myers
109 Model Checking the World Wide Web Luca de Alfaro
111 Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM Marta Kwiatkowska, Gethin Norman and Roberto Segala
118 Using Timestamping and History Variables to Verify Sequential Consistency Tamarah Arons
121 Finite Instantiations in Equivalence Logic with Uninterpreted Functions Yoav Rodeh Ofer Shtrichman
123 Fast LTL to Buchi Automata Translation Paul Gastin and Denis Oddoux
125 Certifying Model Checkers Kedar Namjoshi
126 Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers Per Bjesse (Chalmers), Tim Leonard (Compaq), Abdel Mokkedem (Compaq)
129 Iterating transducers Dennis Dams, Yassine Lakhnech and Martin Steffen
130 Parameterized Verification with Automatically Computed Inductive Assertions T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck
136 Symmetry and Reduced Symmetry in Model-checking Patrice Godefroid, A. Prasad Sistla
137 Distributed Model Checking for mu-calculus Orna Grumberg, Tamir Heyman, Assaf Schuster
138 Transformation-Based Verification Using Generalized Retiming Andreas Kuehlmann Jason Baumgartner
140 Job-Shop Scheduling usinf Timed Automata Yasmina Abdeddaim and Oded Maler

Tool Presentations

1010 The Temporal Logic Sugar Ilan Beer Shoham Ben-David Cindy Eisner Dana Fisman Anna Gringauze Yoav Rodeh
1011 mCRL: A Toolset to Analyse Algebraic Specifications Stefan Blom, Wan Fokkink, Jan Friso Groote, Izak van Langevelde, Bert Lisser, Jaco van de Pol
1015 Computing One-to-One Minimum-Width Abstractions of Digital Designs for RTL Property Checking Peer Johannsen
1021 SDLcheck: A Model Checking Tool Vladimir Levin, Husnu Yenigun
1045 Truth/SLC - A Parallel Verification Platform for Concurrent Systems Martin Leucker and Thomas Noll
1048 EASN: Integrating ASN.1 and Model Checking Vivek K. Shanbhag, K. Gopinath, Markku Turunen, Ari Ahtiainen, Matti Luukkainen
1082 RTDT: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams Nina Amla, E. Allen Emerson, Robert P. Kurshan and Kedar Namjoshi
1086 The SLAM Toolkit Thomas Ball Sriram K. Rajamani
1095 ICS: Integrated Canonizer and Solver Jean-Christophe Filliatre, Sam Owre, Harald Ruess, N. Shankar
1106 AGVI -- Automatic Generation, Verification, and Implementation of Security Protocols Dawn Song and Adrian Perrig
1114 TAXYS : a Tool for Developing and Verifying Real-Time Properties of Embedded Systems Daniel Weil, Etienne Closse, Michel Poize, Patrick Venier and Jacques Pulou (France Telecom R&D), Sergio Yovine and Joseph Sifakis (VERIMAG)
1128 EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality and Conservative Transformations Miroslav N. Velev Randal E. Bryant
1141 TReX: A Tool for Reachability Analysis of Complex Systems Aurore Annichini, Ahmed Bouajjani, and Mihaela Sighireanu