Front matter
1
Software Documentation and the Verification Process
David Lorge Parnas
2-13
Certifying Model Checkers
Kedar S. Namjoshi
14-24
Formalizing a JVML Verifier for Initialization in a Theorem Prover
Yves Bertot
25-37
Automated Inductive Verification of Parameterized Protocols?
Abhik Roychoudhury and I.V. Ramakrishnan
38-52
Efficient Model Checking Via Büchi Tableau Automata?
Girish S. Bhat, Rance Cleaveland and Alex Groce
53-65
Fast LTL to Büchi Automata Translation
Paul Gastin and Denis Oddoux
66-78
A Practical Approach to Coverage in Model Checking
Hana Chockler, Orna Kupferman, Robert P. Kurshan and Moshe Y. Vardi
79-90
A Fast Bisimulation Algorithm
Agostino Dovier, Carla Piazza and Alberto Policriti
91-103
Symmetry and Reduced Symmetry in Model Checking?
A. Prasad Sistla and Patrice Godefroid
104-117
Transformation-Based Verification Using Generalized Retiming
Andreas Kuehlmann and Jason Baumgartner
118-130
Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions
Gianpiero Cabodi
131-143
CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination
John Moondanos, Carl H. Seger, Ziyad Hanna and Daher Kaiss
144-154
Finite Instantiations in Equivalence Logic with Uninterpreted Functions
Yoav Rodeh and Ofer Shtrichman
155-168
Model Checking with Formula-Dependent Abstract Models
Alexander Asteroth, Christel Baier and Ulrich A*Bmann
169-181
Verifying Network Protocol Implementations by Symbolic Refinement Checking
Rajeev Alur and Bow-Yaw Wang
182-193
Automatic Abstraction for Verification of Timed Circuits and Systems?
Hao Zheng, Eric Mercer and Chris Myers
194-206
Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM?
Marta Kwiatkowska, Gethin Norman and Roberto Segala
207-220
Analysis of Recursive State Machines
Rajeev Alur, Kousha Etessami and Mihalis Yannakakis
221-234
Parameterized Verification with Automatically Computed Inductive Assertions?
Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Ying Xu and Lenore Zuck
235-240
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations
Miroslav N. Velev and Randal E. Bryant
241-245
AGVI — Automatic Generation, Verification, and Implementation of Security Protocols
Dawn Song, Adrian Perrig and Doantam Phan
246-249
ICS: Integrated Canonizer and Solver?
Jean-Christophe Filliâtre, Sam Owre, Harald Rue*B and Natarajan Shankar
250-254
µCRL: A Toolset for Analysing Algebraic Specifications
Stefan Blom, Wan Fokkink, Jan Friso Groote, Izak van Langevelde and Bert Lisser, et al.
255-259
Truth/SLC — A Parallel Verification Platform for Concurrent Systems
Martin Leucker and Thomas Noll
260-264
The SLAM Toolkit
Thomas Ball and Sriram K. Rajamani
265-285
Java Bytecode Verification: An Overview
Xavier Leroy
286-297
Iterating Transducers
Dennis Dams, Yassine Lakhnech and Martin Steffen
298-310
Attacking Symbolic State Explosion
Giorgio Delzanno, Jean-François Raskin and Laurent Van Begin
311-323
A Unifying Model Checking Approach for Safety Properties of Parameterized Systems
Monika Maidl
324-336
A BDD-Based Model Checker for Recursive Programs
Javier Esparza and Stefan Schwoon
337-349
Model Checking the World Wide Web?
Luca de Alfaro
350-362
Distributed Symbolic Model Checking for μ-Calculus
Orna Grumberg, Tamir Heyman and Assaf Schuster
363-367
The Temporal Logic Sugar
Ilan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman and Anna Gringauze, et al.
368-372
TReX: A Tool for Reachability Analysis of Complex Systems
Aurore Annichini, Ahmed Bouajjani and Mihaela Sighireanu
373-377
BOOSTER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstraction
Peer Johannsen
378-381
SDLcheck: A Model Checking Tool
Vladimir Levin and Hüsnü Yenigün
382-386
EASN: Integrating ASN.1 and Model Checking
Vivek K. Shanbhag, K. Gopinath, Markku Turunen, Ari Ahtiainen and Matti Luukkainen
387-390
Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams
Nina Amla, E. Allen Emerson, Robert P. Kurshan and Kedar Namjoshi
391-395
TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems?
Etienne Closse, Michel Poize, Jacques Pulou, Joseph Sifakis and Patrick Venter, et al.
396-410
Microarchitecture Verification by Compositional Model Checking
Ranjit Jhala1 and Kenneth L. McMillan
411-422
Rewriting for Symbolic Execution of State Machine Models
J. Strother Moore
423-435
Using Timestamping and History Variables to Verify Sequential Consistency
Tamarah Arons
436-453
Benefits of Bounded Model Checking at an Industrial Setting
Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia and Gila Kamhi, et al.
454-464
Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers
Per Bjesse, Tim Leonard and Abdel Mokkedem
465-477
Towards Efficient Verification of Arithmetic Algorithms over Galois Fields
GF
(2m)
Sumio Morioka, Yasunao Katayama and Toshiyuki Yamane
478-492
Job-Shop Scheduling Using Timed Automata?
Yasmina Abdeddaïm and Oded Maler
493-505
As Cheap as Possible: Effcient Cost-Optimal Reachability for Priced Timed Automata
Kim Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker and Thomas Hune, et al.
506-517
Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks
Zhe Dang
Back matter