Correct Hardware Design and Verification Methods: 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001 Livingston, Scotland, UK, September 4–7, 2001 ProceedingsAuthor: Tiziana Margaria, Tom Melham Published by Springer Berlin Heidelberg ISBN: 978-3-540-42541-0 DOI: 10.1007/3-540-44798-9Table of Contents:View from the Fringe of the Fringe Hardware Synthesis Using SAFL and Application to Processor Design Applications of Hierarchical Verification in Model Checking Pruning Techniques for the SAT-Based Bounded Model Checking Problem Heuristics for Hierarchical Partitioning with Application to Model Checking Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs Deriving Real-Time Programs from Duration Calculus Specifications Reproducing Synchronization Bugs with Model Checking Formally-Based Design Evaluation Multiclock Esterel Register Transformations with Multiple Clock Domains Temporal Properties of Self-Timed Rings Coverability Analysis Using Symbolic Model Checking Specifying Hardware Timing with ET-Lotos Formal Pipeline Design Verification of Basic Block Schedules Using RTL Transformations Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking Proof Engineering in the Large: Formal Verification of Pentium®4 Floating-Point Divider Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques A Higher-Level Language for Hardware Synthesis, Includes bibliographical references and index