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

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2002.
1 online resource (X, 362 pages)
1st ed. 2002.
Computer Science (Springer-11645)
Lecture notes in computer science 0302-9743 ; 2404
Lecture Notes in Computer Science, 0302-9743 ; 2404
Contained In:
Springer eBooks

Location Notes Your Loan Policy


Computer logic.
Software engineering.
Logic, Symbolic and mathematical.
Artificial intelligence.
Computers, Special purpose.
Local subjects:
Theory of Computation. (search)
Logics and Meanings of Programs. (search)
Software Engineering. (search)
Mathematical Logic and Formal Languages. (search)
Artificial Intelligence. (search)
Special Purpose and Application-Based Systems. (search)
System Details:
text file PDF
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.
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.
Brinksma, Ed, editor., Editor,
Larsen, Kim G. editor., Editor,
SpringerLink (Online service)
Other format:
Printed edition:
Printed edition:
Publisher Number:
10.1007/3-540-45657-0 doi
Access Restriction:
Restricted for use by site license.