Computer aided verification : ; proceedings 12th international conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000
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...
Gardado en:
| Autor Corporativo: | |
|---|---|
| Outros autores: | , |
| Formato: | Livre numérique |
| Idioma: | Anglais |
| Publicado: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Series: | Lecture notes in computer science
1855 |
| Sujets: | |
| Acceso en liña: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Nota: |
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, 12th international conference, CAV 2000, Chicago, IL, USA, July 15-19, 2000, E. Allen Emerson, A. Prasad Sistla (eds.), 2000, Berlin, Springer, 1 vol. (X-582 p.), Lecture notes in computer science, 3-540-67770-4 • Computer Aided Verification, Texte imprimé, 9783662186701 |
Table des matières:
- 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 TraceTheoretic Verification of Timed Asynchronous Circuits
- XMC: A Logic-Programming-Based Verification Toolset.