Correct Hardware Design and Verification Methods 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005. Proceedings /
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2005.
|
| Σειρά: | Lecture Notes in Computer Science,
3725 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- Invited Talks
- Is Formal Verification Bound to Remain a Junior Partner of Simulation?
- Verification Challenges in Configurable Processor Design with ASIP Meister
- Tutorial
- Towards the Pervasive Verification of Automotive Systems
- Functional Approaches to Design Description
- Wired: Wire-Aware Circuit Design
- Formalization of the DE2 Language
- Game Solving Approaches
- Finding and Fixing Faults
- Verifying Quantitative Properties Using Bound Functions
- Abstraction
- How Thorough Is Thorough Enough?
- Interleaved Invariant Checking with Dynamic Abstraction
- Automatic Formal Verification of Liveness for Pipelined Processors with Multicycle Functional Units
- Algorithms and Techniques for Speeding (DD-Based) Verification 1
- Efficient Symbolic Simulation via Dynamic Scheduling, Don’t Caring, and Case Splitting
- Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation
- Saturation-Based Symbolic Reachability Analysis Using Conjunctive and Disjunctive Partitioning
- Real Time and LTL Model Checking
- Real-Time Model Checking Is Really Simple
- Temporal Modalities for Concisely Capturing Timing Diagrams
- Regular Vacuity
- Algorithms and Techniques for Speeding Verification 2
- Automatic Generation of Hints for Symbolic Traversal
- Maximal Input Reduction of Sequential Netlists via Synergistic Reparameterization and Localization Strategies
- A New SAT-Based Algorithm for Symbolic Trajectory Evaluation
- Evaluation of SAT-Based Tools
- An Analysis of SAT-Based Model Checking Techniques in an Industrial Environment
- Model Reduction
- Exploiting Constraints in Transformation-Based Verification
- Identification and Counter Abstraction for Full Virtual Symmetry
- Verification of Memory Hierarchy Mechanisms
- On the Verification of Memory Management Mechanisms
- Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification
- Short Papers
- Symbolic Partial Order Reduction for Rule Based Transition Systems
- Verifying Timing Behavior by Abstract Interpretation of Executable Code
- Behavior-RTL Equivalence Checking Based on Data Transfer Analysis with Virtual Controllers and Datapaths
- Deadlock Prevention in the Æthereal Protocol
- Acceleration of SAT-Based Iterative Property Checking
- Error Detection Using BMC in a Parallel Environment
- Formal Verification of Synchronizers
- A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems
- Improvements to the Implementation of Interpolant-Based Model Checking
- High-Level Modelling, Analysis, and Verification on FPGA-Based Hardware Design
- Proving Parameterized Systems: The Use of Pseudo-Pipelines in Polyhedral Logic
- Resolving Quartz Overloading
- FPGA Based Accelerator for 3-SAT Conflict Analysis in SAT Solvers
- Predictive Reachability Using a Sample-Based Approach
- Minimizing Counterexample of ACTL Property
- Data Refinement for Synchronous System Specification and Construction
- Introducing Abstractions via Rewriting
- A Case Study: Formal Verification of Processor Critical Properties.
