Computer Aided Verification 12th International Conference, CAV 2000 Chicago, IL, USA, July 15-19, 2000 Proceedings /
This volume contains the proceedings of the 12th International Conference on Computer Aided Veri?cation (CAV 2000) held in Chicago, Illinois, USA during 15-19 July 2000. The CAV conferences are devoted to the advancement of the theory and practice of formal methods for hardware and software veri?cat...
| Corporate Author: | |
|---|---|
| Other Authors: | , |
| Format: | Electronic eBook |
| Language: | English |
| Published: |
Berlin, Heidelberg :
Springer Berlin Heidelberg : Imprint: Springer,
2000.
|
| Edition: | 1st ed. 2000. |
| Series: | Lecture Notes in Computer Science,
1855 |
| Subjects: | |
| Online Access: | Full Text via HEAL-Link |
Table of Contents:
- Invited Talks and Tutorials
- Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion
- Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis
- Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation
- Invited Tutorial: Verification of Infinite-state and Parameterized Systems
- Regular Papers
- An Abstraction Algorithm for the Verification of Generalized C-Slow Designs
- Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits
- An Automata-Theoretic Approach to Reasoning about Infinite-State Systems
- Automatic Verification of Parameterized Cache Coherence Protocols
- Binary Reachability Analysis of Discrete Pushdown Timed Automata
- Boolean Satisfiability with Transitivity Constraints
- Bounded Model Construction for Monadic Second-Order Logics
- Building Circuits from Relations
- Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking
- On the Completeness of Compositional Reasoning
- Counterexample-Guided Abstraction Refinement
- Decision Procedures for Inductive Boolean Functions Based on Alternating Automata
- Detecting Errors Before Reaching Them
- A Discrete Strategy Improvement Algorithm for Solving Parity Games
- Distributing Timed Model Checking - How the Search Order Matters
- Efficient Algorithms for Model Checking Pushdown Systems
- Efficient Büchi Automata from LTL Formulae
- Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods
- Efficient Reachability Analysis of Hierarchical Reactive Machines
- Formal Verification of VLIW Microprocessors with Speculative Execution
- Induction in Compositional Model Checking
- Liveness and Acceleration in Parameterized Verification
- Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm
- Model Checking Continuous-Time Markov Chains by Transient Analysis
- Model-Checking for Hybrid Systems by Quotienting and Constraints Solving
- Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification
- Regular Model Checking
- Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems
- Syntactic Program Transformations for Automatic Abstraction
- Temporal-logic Queries
- Are Timed Automata Updatable?
- Tuning SAT Checkers for Bounded Model Checking
- Unfoldings of Unbounded Petri Nets
- Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification
- Verifying Advanced Microarchitectures that Support Speculation and Exceptions
- Tool Papers
- FoCs - Automatic Generation of Simulation Checkers from Formal Specifications
- IF: A Validation Environment for Timed Asynchronous Systems
- Integrating WS1S with PVS
- PET: An Interactive Software Testing Tool
- A Proof-Carrying Code Architecture for Java
- The Statemate Verification Environment
- TAPS: A First-Order Verifier for Cryptographic Protocols
- VINAS-P: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits
- XMC: A Logic-Programming-Based Verification Toolset.
