Correct Hardware Design and Verification Methods 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001 Livingston, Scotland, UK, September 4-7, 2001 Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Margaria, Tiziana (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Melham, Tom (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2001.
• Έκδοση: 1st ed. 2001.
• Σειρά: Lecture Notes in Computer Science, 2144
• Θέματα: Architecture, Computer.; Computers.; Software engineering.; Computer hardware.; Computer logic.; Computer System Implementation.; Theory of Computation.; Software Engineering/Programming and Operating Systems.; Computer Hardware.; Logics and Meanings of Programs.; Software Engineering.

This volume contains the proceedings of CHARME 2001, the Eleventh Advanced Research Working Conference on Correct Hardware Design and Veri?cation Methods. CHARME 2001 is the 11th in a series of working conferences devoted to the development and use of leading-edge formal techniques and tools for the...

Πίνακας περιεχομένων:

• Invited Contributions
• View from the Fringe of the Fringe
• Hardware Synthesis Using SAFL and Application to Processor Design
• FMCAD 2000
• Applications of Hierarchical Verification in Model Checking
• Model Checking 1
• Pruning Techniques for the SAT-Based Bounded Model Checking Problem
• Heuristics for Hierarchical Partitioning with Application to Model Checking
• Short Papers 1
• 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
• Clocking Issues
• Multiclock Esterel
• Register Transformations with Multiple Clock Domains
• Temporal Properties of Self-Timed Rings
• Short Papers 2
• Coverability Analysis Using Symbolic Model Checking
• Specifying Hardware Timing with ET-Lotos
• Formal Pipeline Design
• Verification of Basic Block Schedules Using RTL Transformations
• Joint Session with TPHOLs
• 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
• Hardware Compilation
• Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques
• A Higher-Level Language for Hardware Synthesis
• Tools
• Hierarchical Verification Using an MDG-HOL Hybrid Tool
• Exploiting Transition Locality in Automatic Verification
• Efficient Debugging in a Formal Verification Environment
• Model Checking 2
• Using Combinatorial Optimization Methods for Quantification Scheduling
• Net Reductions for LTL Model-Checking
• Component Verification
• Formal Verification of the VAMP Floating Point Unit
• A Specification Methodology by a Collection of Compact Properties as Applied to the Intel® Itanium™ Processor Bus Protocol
• The Design and Verification of a Sorter Core
• Case Studies
• Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip
• Using Abstract Specifications to Verify PowerPC™ Custom Memories by Symbolic Trajectory Evaluation
• Algorithm Verification
• Formal Verification of Conflict Detection Algorithms
• Induction-Oriented Formal Verification in Symmetric Interconnection Networks
• A Framework for Microprocessor Correctness Statements
• Duration Calculus
• From Operational Semantics to Denotational Semantics for Verilog
• Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming.