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

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Brinksma, Ed (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Larsen, Kim G. (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2002.
• Έκδοση: 1st ed. 2002.
• Σειρά: Lecture Notes in Computer Science, 2404
• Θέματα: Computers.; Computer logic.; Software engineering.; Mathematical logic.; Artificial intelligence.; Special purpose computers.; Theory of Computation.; Logics and Meanings of Programs.; Software Engineering.; Mathematical Logic and Formal Languages.; Artificial Intelligence.; Special Purpose and Application-Based Systems.

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

Πίνακας περιεχομένων:

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