13. CAV 2001: Paris, France

Gérard Berry, Hubert Comon, Alain Finkel (Eds.): Computer Aided Verification, 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001, Proceedings. Lecture Notes in Computer Science 2102 Springer 2001, ISBN 3-540-42345-1

Invited Talk

Kedar S. Namjoshi:
Certifying Model Checkers. 2-13
Yves Bertot:
Formalizing a JVML Verifier for Initialization in a Theorem Prover. 14-24
Abhik Roychoudhury, I. V. Ramakrishnan:
Automated Inductive Verification of Parameterized Protocols. 25-37

Girish Bhat, Rance Cleaveland, Alex Groce:
Efficient Model Checking Via Büchi Tableau Automata. 38-52
Paul Gastin, Denis Oddoux:
Fast LTL to Büchi Automata Translation. 53-65
Hana Chockler, Orna Kupferman, Robert P. Kurshan, Moshe Y. Vardi:
A Practical Approach to Coverage in Model Checking. 66-78

Agostino Dovier, Carla Piazza, Alberto Policriti:
A Fast Bisimulation Algorithm. 79-90
A. Prasad Sistla, Patrice Godefroid:
Symmetry and Reduced Symmetry in Model Checking. 91-103
Andreas Kuehlmann, Jason Baumgartner:
Transformation-Based Verification Using Generalized Retiming. 104-117

Gianpiero Cabodi:
Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions. 118-130
John Moondanos, Carl-Johan H. Seger, Ziyad Hanna, Daher Kaiss:
CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination. 131-143
Yoav Rodeh, Ofer Strichman:
Finite Instantiations in Equivalence Logic with Uninterpreted Functions. 144-154

Alexander Asteroth, Christel Baier, Ulrich Aßmann:
Model Checking with Formula-Dependent Abstract Models. 155-168
Rajeev Alur, Bow-Yaw Wang:
Verifying Network Protocol Implementations by Symbolic Refinement Checking. 169-181
Hao Zheng, Eric Mercer, Chris J. Myers:
Automatic Abstraction for Verification of Timed Circuits and Systems. 182-193

Marta Z. Kwiatkowska, Gethin Norman, Roberto Segala:
Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM. 194-206
Rajeev Alur, Kousha Etessami, Mihalis Yannakakis:
Analysis of Recursive State Machines. 207-220
Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck:
Parameterized Verification with Automatically Computed Inductive Assertions. 221-234

Miroslav N. Velev, Randal E. Bryant:
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations. 235-240
Dawn Xiaodong Song, Adrian Perrig, Doantam Phan:
AGVI - Automatic Generation, Verification, and Implementation of Security Protocols. 241-245
Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, Natarajan Shankar:
ICS: Integrated Canonizer and Solver. 246-249
Stefan Blom, Wan Fokkink, Jan Friso Groote, Izak van Langevelde, Bert Lisser, Jaco van de Pol:
µCRL: A Toolset for Analysing Algebraic Specifications. 250-254
Martin Leucker, Thomas Noll:
Truth/SLC - A Parallel Verification Platform for Concurrent Systems. 255-259
Thomas Ball, Sriram K. Rajamani:
The SLAM Toolkit. 260-264

Dennis Dams, Yassine Lakhnech, Martin Steffen:
Iterating Transducers. 286-297
Giorgio Delzanno, Jean-François Raskin, Laurent Van Begin:
Attacking Symbolic State Explosion. 298-310
Monika Maidl:
A Unifying Model Checking Approach for Safety Properties of Parameterized Systems. 311-323
Javier Esparza, Stefan Schwoon:
A BDD-Based Model Checker for Recursive Programs. 324-336

Luca de Alfaro:
Model Checking the World Wide Web. 337-349
Orna Grumberg, Tamir Heyman, Assaf Schuster:
Distributed Symbolic Model Checking for µ-Calculus. 350-362

Ilan Beer, Shoham Ben-David, Cindy Eisner, Dana Fisman, Anna Gringauze, Yoav Rodeh:
The Temporal Logic Sugar. 363-367
Aurore Annichini, Ahmed Bouajjani, Mihaela Sighireanu:
TReX: A Tool for Reachability Analysis of Complex Systems. 368-372
Peer Johannsen:
BooStER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstarction. 373-377
Vladimir Levin, Hüsnü Yenigün:
SDLcheck: A Model Checking Tool. 377
Vivek K. Shanbhag, K. Gopinath, Markku Turunen, Ari Ahtiainen, Matti Luukkainen:
EASN: Integrating ASN.1 and Model Checking. 382-386
Nina Amla, E. Allen Emerson, Robert P. Kurshan, Kedar S. Namjoshi:
Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams. 387-390
Etienne Closse, Michel Poize, Jacques Pulou, Joseph Sifakis, Patrick Venter, Daniel Weil, Sergio Yovine:
TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems. 391-395

Ranjit Jhala, Kenneth L. McMillan:
Microarchitecture Verification by Compositional Model Checking. 396-410
J. Strother Moore:
Rewriting for Symbolic Execution of State Machine Models. 411-422
Tamarah Arons:
Using Timestamping and History Variables to Verify Sequential Consistency. 423-435

Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, Moshe Y. Vardi:
Benefits of Bounded Model Checking at an Industrial Setting. 436-453
Per Bjesse, Tim Leonard, Abdel Mokkedem:
Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. 454-464
Sumio Morioka, Yasunao Katayama, Toshiyuki Yamane:
Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2^m). 465-477

Yasmina Abdeddaïm, Oded Maler:
Job-Shop Scheduling Using Timed Automata. 478-492
Kim Guldstrand Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, Judi Romijn:
As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. 493-505
Zhe Dang:
Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks. 506-518

Last update Sat May 18 00:52:46 2013 CET by the DBLP Team —

Data released under the ODC-BY 1.0 license — See also our legal information page