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 |