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

Computer Aided Verification 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001. Proceedings / edited by Gerard Berry, Hubert Comon, Alain Finkel.

Saved in:
Bibliographic Details
Corporate Author: SpringerLink (Online service)
Other Authors: Berry, Gerard (Editor), Comon, Hubert (Editor), Finkel, Alain (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2001.
Edition:1st ed. 2001.
Series:Lecture Notes in Computer Science, 2102
Springer eBook Collection.
Subjects:
Database management.
Computers.
Software engineering.
Computer logic.
Mathematical logic.
Artificial intelligence.
Electronic resources (E-books)
Online Access:Click to view e-book
Holy Cross Note:Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.
Table of Contents:
  • Invited Talk
  • Software Documentation and the Verification Process
  • Model Checking and Theorem Proving
  • Certifying Model Checkers
  • Formalizing a JVML Verifier for Initialization in a Theorem Prover
  • Automated Inductive Verification of Parameterized Protocols?
  • Automata Techniques
  • Efficient Model Checking Via Büchi Tableau Automata?
  • Fast LTL to Büchi Automata Translation
  • A Practical Approach to Coverage in Model Checking
  • Verification Core Technology
  • A Fast Bisimulation Algorithm
  • Symmetry and Reduced Symmetry in Model Checking?
  • Transformation-Based Verification Using Generalized Retiming
  • BDD and Decision Procedures
  • 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
  • Abstraction and Refinement
  • Model Checking with Formula-Dependent Abstract Models
  • Verifying Network Protocol Implementations by Symbolic Refinement Checking
  • Automatic Abstraction for Verification of Timed Circuits and Systems?
  • Combinations
  • 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?
  • Tool Presentations: Rewriting and Theorem-Proving Techniques
  • EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations
  • AGVI — Automatic Generation, Verification, and Implementation of Security Protocols
  • ICS: Integrated Canonizer and Solver?
  • µCRL: A Toolset for Analysing Algebraic Specifications
  • Truth/SLC — A Parallel Verification Platform for Concurrent Systems
  • The SLAM Toolkit
  • Invited Talk
  • Java Bytecode Verification: An Overview
  • Infinite State Systems
  • Iterating Transducers
  • Attacking Symbolic State Explosion
  • A Unifying Model Checking Approach for Safety Properties of Parameterized Systems
  • A BDD-Based Model Checker for Recursive Programs
  • Temporal Logics and Verification
  • Model Checking the World Wide Web?
  • Distributed Symbolic Model Checking for ?-Calculus
  • Tool Presentations: Model-Checking and Automata Techniques
  • The Temporal Logic Sugar
  • TReX: A Tool for Reachability Analysis of Complex Systems
  • BOOSTER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstraction
  • SDLcheck: A Model Checking Tool
  • EASN: Integrating ASN.1 and Model Checking
  • Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams
  • TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems?
  • Microprocessor Verification, Cache Coherence
  • Microarchitecture Verification by Compositional Model Checking
  • Rewriting for Symbolic Execution of State Machine Models
  • Using Timestamping and History Variables to Verify Sequential Consistency
  • SAT, BDDs, and Applications
  • Benefits of Bounded Model Checking at an Industrial Setting
  • Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers
  • Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m)
  • Timed Automata
  • Job-Shop Scheduling Using Timed Automata?
  • As Cheap as Possible: Effcient Cost-Optimal Reachability for Priced Timed Automata
  • Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks.

Similar Items