Computer Aided Verification: 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 Proceedings

Software Documentation and the Verification Process....Pages 1-1
Certifying Model Checkers....Pages 2-13
Formalizing a JVML Verifier for Initialization in a Theorem Prover....Pages 14-24
Automated Inductive Verification of Parameterized Protocols?....Pages 25-37
Efficient Model Checking Via Büchi Tableau Automata?....Pages 38-52
Fast LTL to Büchi Automata Translation....Pages 53-65
A Practical Approach to Coverage in Model Checking....Pages 66-78
A Fast Bisimulation Algorithm....Pages 79-90
Symmetry and Reduced Symmetry in Model Checking?....Pages 91-103
Transformation-Based Verification Using Generalized Retiming....Pages 104-117
Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions....Pages 118-130
CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination....Pages 131-143
Finite Instantiations in Equivalence Logic with Uninterpreted Functions....Pages 144-154
Model Checking with Formula-Dependent Abstract Models....Pages 155-168
Verifying Network Protocol Implementations by Symbolic Refinement Checking....Pages 169-181
Automatic Abstraction for Verification of Timed Circuits and Systems?....Pages 182-193
Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM?....Pages 194-206
Analysis of Recursive State Machines....Pages 207-220
Parameterized Verification with Automatically Computed Inductive Assertions?....Pages 221-234
EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations....Pages 235-240
AGVI — Automatic Generation, Verification, and Implementation of Security Protocols....Pages 241-245
ICS: Integrated Canonizer and Solver?....Pages 246-249
µCRL: A Toolset for Analysing Algebraic Specifications....Pages 250-254
Truth/SLC — A Parallel Verification Platform for Concurrent Systems....Pages 255-259
The SLAM Toolkit....Pages 260-264
Java Bytecode Verification: An Overview....Pages 265-285
Iterating Transducers....Pages 286-297
Attacking Symbolic State Explosion....Pages 298-310
A Unifying Model Checking Approach for Safety Properties of Parameterized Systems....Pages 311-323
A BDD-Based Model Checker for Recursive Programs....Pages 324-336
Model Checking the World Wide Web?....Pages 337-349
Distributed Symbolic Model Checking for μ-Calculus....Pages 350-362
The Temporal Logic Sugar....Pages 363-367
TReX: A Tool for Reachability Analysis of Complex Systems....Pages 368-372
BOOSTER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstraction....Pages 373-377
SDLcheck: A Model Checking Tool....Pages 378-381
EASN: Integrating ASN.1 and Model Checking....Pages 382-386
Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams....Pages 387-390
TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems?....Pages 391-395
Microarchitecture Verification by Compositional Model Checking....Pages 396-410
Rewriting for Symbolic Execution of State Machine Models....Pages 411-422
Using Timestamping and History Variables to Verify Sequential Consistency....Pages 423-435
Benefits of Bounded Model Checking at an Industrial Setting....Pages 436-453
Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers....Pages 454-464
Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF (2 m )....Pages 465-477
Job-Shop Scheduling Using Timed Automata?....Pages 478-492
As Cheap as Possible: Effcient Cost-Optimal Reachability for Priced Timed Automata....Pages 493-505
Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks....Pages 506-517