Correct Hardware Design and Verification Methods: 13th IFIP WG 10.5Advanced Research, Working Conference, CHARME 2005, Saarbrücken, Germany, October 3-6, 2005, Proceedings: Lecture Notes in Computer Science, cartea 3725

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 Verificationof 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.