Computer Aided Verification: 13th International Conference, Cav 2001, Paris, France, July 18-22, 2001. Proceedings (lecture Notes In Computer Science)

This book constitutes the refereed proceedings of the 13th International Conference on Computer Aided Verification, CAV 2001, held in Paris, France in July 2001. The 33 revised full papers presented were carefully reviewed and selected from 106 regular paper submissions; also included are 13 reviewed tool presentations selected from 27 submissions. The book offers topical sections on model checking and theorem proving, automata techniques, verification core technology, BDD and decision trees, abstraction and refinement, combinations, infinite state systems, temporal logics and verification, microprocessor verification and cache coherence, SAT and applications, and timed automata. 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 The papers in this work cover topics such as: model checking and theorem proving; automata techniques; verification core technology; BDD and decision trees; abstraction and refinement; combinations; infinite state systems; and temporal logics and verification. This book constitutes the proceedings of the 26th International Conference on Computer Aided Verification, CAV 2014, held as part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014.