Coverart for item
The Resource 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, Tiziana Margaria, Tom Melham (eds.)

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, Tiziana Margaria, Tom Melham (eds.)

Label
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
Title
Correct hardware design and verification methods
Title remainder
11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001 : proceedings
Statement of responsibility
Tiziana Margaria, Tom Melham (eds.)
Creator
Contributor
Subject
Genre
Language
eng
Summary
This book constitutes the refereed proceedings of the 11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2001, held in Livingston, Scotland, UK in September 2001. The 28 revised full papers and eight short papers presented together with two invited papers and one special paper were carefully reviewed and selected from 56 submissions. The book offers topical sections on model checking, clocking issues, theorem proving with higher order logics, hardware compilation, tools, component verification, case studies, algorithm verification, and duration calculus
Member of
Cataloging source
YNG
Dewey number
621.395
Index
index present
LC call number
TK7874.75
LC item number
.C453 2001eb
Literary form
non fiction
http://bibfra.me/vocab/lite/meetingDate
2001
http://bibfra.me/vocab/lite/meetingName
CHARME 2001
Nature of contents
  • dictionaries
  • bibliography
http://library.link/vocab/relatedWorkOrContributorDate
1964-
http://library.link/vocab/relatedWorkOrContributorName
  • Margaria-Steffen, Tiziana
  • Melham, T. F.
Series statement
Lecture notes in computer science
Series volume
2144
http://library.link/vocab/subjectName
  • Integrated circuits
  • Integrated circuits
  • Integrated circuits
  • Integrated circuits
Target audience
adult
Label
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, Tiziana Margaria, Tom Melham (eds.)
Instantiates
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
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{u2122} 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{u2122} 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
Control code
644364586
Dimensions
unknown
Extent
1 online resource (xii, 482 pages).
File format
multiple file formats
Form of item
online
Isbn
9783540447986
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Reformatting quality
access
Specific material designation
remote
System control number
(OCoLC)644364586
Label
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, Tiziana Margaria, Tom Melham (eds.)
Publication
Bibliography note
Includes bibliographical references and index
Carrier category
online resource
Carrier category code
  • cr
Carrier MARC source
rdacarrier
Content category
text
Content type code
  • txt
Content type MARC source
rdacontent
Contents
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{u2122} 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{u2122} 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
Control code
644364586
Dimensions
unknown
Extent
1 online resource (xii, 482 pages).
File format
multiple file formats
Form of item
online
Isbn
9783540447986
Media category
computer
Media MARC source
rdamedia
Media type code
  • c
Reformatting quality
access
Specific material designation
remote
System control number
(OCoLC)644364586

Library Locations

    • Ellis LibraryBorrow it
      1020 Lowry Street, Columbia, MO, 65201, US
      38.944491 -92.326012
Processing Feedback ...