Computer aided verification : 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27 31, 2002 : proceedings
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...
保存先:
| 団体著者: | |
|---|---|
| その他の著者: | , |
| フォーマット: | Livre numérique |
| 言語: | Anglais |
| 出版事項: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| シリーズ: | Lecture notes in computer science
2404 |
| 主題: | |
| オンライン･アクセス: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| 注記: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Computer aided verification, 14th International Conference, CAV 2002, Copenhagen, Denmark, July 27-31, 2002, proceedings, Ed Brinksma, Kim Guldstrand Larsen (eds.), Berlin, Springer, 2002, 1 vol. (XIII-626 p.), Lecture notes in computer science, 3-540-43997-8 • Computer Aided Verification, Texte imprimé, 9783662188866 |
目次:
- 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 HybridSystems
- 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 SystemsCode
- 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.