Computer aided verification : 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002 : proceedings

Ed Brinksma, Kim Guldstrand Larsen (eds.)

This book constitutes the refereed proceedings of the 14th International Conference on Computer Aided Verification, CAV 2002, held in Copenhagen, Denmark in July 2002. The 35 revised full papers presented together with five invited contributions and 11 tool presentations were carefully reviewed and selected from 94 submissions. The papers are organized in topical sections in symbolic model checking, abstraction/refinement and model checking, compositional/structural verification, timing analysis, SAT based methods, infinite state model checking, extended model checking, code verification, regular model checking and acceleration, and model reduction.

「Nielsen BookData」より


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

「Nielsen BookData」より


書名 Computer aided verification : 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002 : proceedings
著作者等 Brinksma, Ed
Larsen, K. G.
Larsen Kim G.
Brinksma Ed.
書名別名 Computer aided verification : 14th International Conference, CAV 2002, Copenhagen, Denmark, July 2002 : proceedings
シリーズ名 Lecture notes in computer science
出版元 Springer
刊行年月 c2002
ページ数 xiii, 626 p.
大きさ 24 cm
ISBN 3540439978
NCID BA58064487
※クリックでCiNii Booksを表示
言語 英語
出版国 ドイツ