Computer Aided Verification 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27-31, 2002 Proceedings

Computer Aided Verification 14th International Conference, CAV 2002 Copenhagen, Denmark, July 27-31, 2002 Proceedings / edited by Ed Brinksma, Kim G. Larsen.

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...

Full description

Saved in:
Bibliographic Details
Corporate Author: SpringerLink (Online service)
Other Authors: Brinksma, Ed (Editor), Larsen, Kim G. (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2002.
Edition:1st ed. 2002.
Series:Lecture Notes in Computer Science, 2404
Springer eBook Collection.
Subjects:
Computers.
Computer logic.
Software engineering.
Mathematical logic.
Artificial intelligence.
Special purpose computers.
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 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.

Similar Items