| 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 |
| 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 |