Computer aided verification : 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002 : proceedings
Author(s)
Bibliographic Information
Computer aided verification : 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002 : proceedings
(Lecture notes in computer science, 2404)
Springer, c2002
- Other Title
-
Computer aided verification : 14th International Conference, CAV 2002, Copenhagen, Denmark, July 2002 : proceedings
Available at 31 libraries
  Aomori
  Iwate
  Miyagi
  Akita
  Yamagata
  Fukushima
  Ibaraki
  Tochigi
  Gunma
  Saitama
  Chiba
  Tokyo
  Kanagawa
  Niigata
  Toyama
  Ishikawa
  Fukui
  Yamanashi
  Nagano
  Gifu
  Shizuoka
  Aichi
  Mie
  Shiga
  Kyoto
  Osaka
  Hyogo
  Nara
  Wakayama
  Tottori
  Shimane
  Okayama
  Hiroshima
  Yamaguchi
  Tokushima
  Kagawa
  Ehime
  Kochi
  Fukuoka
  Saga
  Nagasaki
  Kumamoto
  Oita
  Miyazaki
  Kagoshima
  Okinawa
  Korea
  China
  Thailand
  United Kingdom
  Germany
  Switzerland
  France
  Belgium
  Netherlands
  Sweden
  Norway
  United States of America
-
Library, Research Institute for Mathematical Sciences, Kyoto University数研
L/N||LNCS||240402034453
Note
Includes bibliographical references and index
Description and Table of Contents
Description
This volume contains the proceedings of the conference on Computer Aided V- i?cation (CAV 2002), held in Copenhagen, Denmark on July 27-31, 2002. CAV 2002 was the 14th in a series of conferences dedicated to the advancement of the theory and practice of computer-assisted formal analysis methods for software and hardware systems. The conference covers the spectrum from theoretical - sults to concrete applications, with an emphasis on practical veri?cation tools, including algorithms and techniques needed for their implementation. The c- ference has traditionally drawn contributions from researchers as well as prac- tioners in both academia and industry. This year we received 94 regular paper submissions out of which 35 were selected. Each submission received an average of 4 referee reviews. In addition, the CAV program contained 11 tool presentations selected from 16 submissions. For each tool presentation, a demo was given at the conference. The large number of tool submissions and presentations testi?es to the liveliness of the ?eld and its applied ?avor.
Table of Contents
Invited Talks.- Software Analysis and Model Checking.- The Quest for Efficient Boolean Satisfiability Solvers.- Invited Tutorials.- On Abstraction in Software Verification.- The Symbolic Approach to Hybrid Systems.- Infinite Games and Verification.- Symbolic Model Checking.- Symbolic Localization Reduction with Reconstruction Layering and Backtracking.- Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions.- Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking.- Abstraction/Refinement and Model Checking.- Liveness with (0,1, ?)- Counter Abstraction.- Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking.- Automatic Abstraction Using Generalized Model Checking.- Compositional/Structural Verification.- Property Checking via Structural Analysis.- Conformance Checking for Models of Asynchronous Message Passing Software.- A Modular Checker for Multithreaded Programs.- Timing Analysis.- Automatic Derivation of Timing Constraints by Failure Analysis.- Deciding Separation Formulas with SAT.- Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling.- SAT Based Methods.- Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT.- Applying SAT Methods in Unbounded Symbolic Model Checking.- SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques.- Semi-formal Bounded Model Checking.- Symbolic Model Checking.- Algorithmic Verification of Invalidation-Based Protocols.- Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving.- Automated Unbounded Verification of Security Protocols.- Tool Presentations.- Exploiting Behavioral Hierarchy for Efficient Model Checking.- IF-2.0: A Validation Environment for Component-Based Real-Time Systems.- The AVISS Security Protocol Analysis Tool.- SPeeDI - A Verification Tool for Polygonal Hybrid Systems.- NuSMV 2: An OpenSource Tool for Symbolic Model Checking.- The d/dt Tool for Verification of Hybrid Systems.- Infinite Model Checking.- Model Checking Linear Properties of Prefix-Recognizable Systems.- Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking.- On Discrete Modeling and Model Checking for Nonlinear Analog Systems.- Compositional/Structural Verification.- Synchronous and Bidirectional Component Interfaces.- Interface Compatibility Checking for Software Modules.- Practical Methods for Proving Program Termination.- Extended Model Checking.- Evidence-Based Model Checking.- Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification.- Vacuum Cleaning CTL Formulae.- Tool Presentations.- CVC: A Cooperating Validity Checker.- ?Chek: A Multi-valued Model-Checker.- PathFinder: A Tool for Design Exploration.- Abstracting C with abC.- AMC: An Adaptive Model Checker.- Code Verification.- Temporal-Safety Proofs for Systems Code.- Regular Model Checking and Acceleration.- Extrapolating Tree Transformations.- Regular Tree Model Checking.- Compressing Transitions for Model Checking.- Model Reduction.- Canonical Prefixes of Petri Net Unfoldings.- State Space Reduction by Proving Confluence.- Fair Simulation Minimization.
by "Nielsen BookData"