Computer Aided Verification 13th International Conference, CAV 2001, Paris, France, July 18-22, 2001. Proceedings /
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg : Imprint: Springer,
2001.
|
| Έκδοση: | 1st ed. 2001. |
| Σειρά: | Lecture Notes in Computer Science,
2102 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- Invited Talk
- Software Documentation and the Verification Process
- Model Checking and Theorem Proving
- Certifying Model Checkers
- Formalizing a JVML Verifier for Initialization in a Theorem Prover
- Automated Inductive Verification of Parameterized Protocols?
- Automata Techniques
- Efficient Model Checking Via Büchi Tableau Automata?
- Fast LTL to Büchi Automata Translation
- A Practical Approach to Coverage in Model Checking
- Verification Core Technology
- A Fast Bisimulation Algorithm
- Symmetry and Reduced Symmetry in Model Checking?
- Transformation-Based Verification Using Generalized Retiming
- BDD and Decision Procedures
- Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions
- CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination
- Finite Instantiations in Equivalence Logic with Uninterpreted Functions
- Abstraction and Refinement
- Model Checking with Formula-Dependent Abstract Models
- Verifying Network Protocol Implementations by Symbolic Refinement Checking
- Automatic Abstraction for Verification of Timed Circuits and Systems?
- Combinations
- Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM?
- Analysis of Recursive State Machines
- Parameterized Verification with Automatically Computed Inductive Assertions?
- Tool Presentations: Rewriting and Theorem-Proving Techniques
- EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations
- AGVI - Automatic Generation, Verification, and Implementation of Security Protocols
- ICS: Integrated Canonizer and Solver?
- µCRL: A Toolset for Analysing Algebraic Specifications
- Truth/SLC - A Parallel Verification Platform for Concurrent Systems
- The SLAM Toolkit
- Invited Talk
- Java Bytecode Verification: An Overview
- Infinite State Systems
- Iterating Transducers
- Attacking Symbolic State Explosion
- A Unifying Model Checking Approach for Safety Properties of Parameterized Systems
- A BDD-Based Model Checker for Recursive Programs
- Temporal Logics and Verification
- Model Checking the World Wide Web?
- Distributed Symbolic Model Checking for ?-Calculus
- Tool Presentations: Model-Checking and Automata Techniques
- The Temporal Logic Sugar
- TReX: A Tool for Reachability Analysis of Complex Systems
- BOOSTER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstraction
- SDLcheck: A Model Checking Tool
- EASN: Integrating ASN.1 and Model Checking
- Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams
- TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems?
- Microprocessor Verification, Cache Coherence
- Microarchitecture Verification by Compositional Model Checking
- Rewriting for Symbolic Execution of State Machine Models
- Using Timestamping and History Variables to Verify Sequential Consistency
- SAT, BDDs, and Applications
- Benefits of Bounded Model Checking at an Industrial Setting
- Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers
- Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m)
- Timed Automata
- Job-Shop Scheduling Using Timed Automata?
- As Cheap as Possible: Effcient Cost-Optimal Reachability for Priced Timed Automata
- Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks.
