Computer Aided Verification: 13th International Conference, CAV 2001 Paris, France, July 18–22, 2001 ProceedingsAuthor: Gérard Berry, Hubert Comon, Alain Finkel Published by Springer Berlin Heidelberg ISBN: 978-3-540-42345-4 DOI: 10.1007/3-540-44585-4Table of Contents:Software Documentation and the Verification Process Certifying Model Checkers Formalizing a JVML Verifier for Initialization in a Theorem Prover Automated Inductive Verification of Parameterized Protocols? Efficient Model Checking Via Büchi Tableau Automata? Fast LTL to Büchi Automata Translation A Practical Approach to Coverage in Model Checking A Fast Bisimulation Algorithm Symmetry and Reduced Symmetry in Model Checking? Transformation-Based Verification Using Generalized Retiming Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination Finite Instantiations in Equivalence Logic with Uninterpreted Functions Model Checking with Formula-Dependent Abstract Models Verifying Network Protocol Implementations by Symbolic Refinement Checking Automatic Abstraction for Verification of Timed Circuits and Systems? Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM? Analysis of Recursive State Machines Parameterized Verification with Automatically Computed Inductive Assertions? EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations