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.)
Resource Information
The item 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.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries.This item is available to borrow from 1 library branch.
Resource Information
The item 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.) represents a specific, individual, material embodiment of a distinct intellectual or artistic creation found in University of Missouri Libraries.
This item is available to borrow from 1 library branch.
- 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
- Language
- eng
- Extent
- 1 online resource (xii, 482 pages).
- 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
- Isbn
- 9783540447986
- 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.)
- Subject
-
- Conference papers and proceedings
- Integrated circuits -- Verification
- Integrated circuits -- Verification
- Integrated circuits -- Verification -- Congresses
- Integrated circuits -- Very large scale integration | Computer-aided design
- Integrated circuits -- Very large scale integration | Computer-aided design
- Integrated circuits -- Very large scale integration | Computer-aided design -- Congresses
- Conference papers and proceedings
- 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
- 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.)
- 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.)
- 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
Subject
- Conference papers and proceedings
- Integrated circuits -- Verification
- Integrated circuits -- Verification
- Integrated circuits -- Verification -- Congresses
- Integrated circuits -- Very large scale integration | Computer-aided design
- Integrated circuits -- Very large scale integration | Computer-aided design
- Integrated circuits -- Very large scale integration | Computer-aided design -- Congresses
- Conference papers and proceedings
Genre
Member of
Library Links
Embed
Settings
Select options that apply then copy and paste the RDF/HTML data fragment to include in your application
Embed this data in a secure (HTTPS) page:
Layout options:
Include data citation:
<div class="citation" vocab="http://schema.org/"><i class="fa fa-external-link-square fa-fw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Correct-hardware-design-and-verification-methods/YqRvoCa8Kzk/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.library.missouri.edu/portal/Correct-hardware-design-and-verification-methods/YqRvoCa8Kzk/">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.)</a></span> - <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.library.missouri.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.library.missouri.edu/">University of Missouri Libraries</a></span></span></span></span></div>
Note: Adjust the width and height settings defined in the RDF/HTML code fragment to best match your requirements
Preview
Cite Data - Experimental
Data Citation of the Item 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.)
Copy and paste the following RDF/HTML data fragment to cite this resource
<div class="citation" vocab="http://schema.org/"><i class="fa fa-external-link-square fa-fw"></i> Data from <span resource="http://link.library.missouri.edu/portal/Correct-hardware-design-and-verification-methods/YqRvoCa8Kzk/" typeof="Book http://bibfra.me/vocab/lite/Item"><span property="name http://bibfra.me/vocab/lite/label"><a href="http://link.library.missouri.edu/portal/Correct-hardware-design-and-verification-methods/YqRvoCa8Kzk/">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.)</a></span> - <span property="potentialAction" typeOf="OrganizeAction"><span property="agent" typeof="LibrarySystem http://library.link/vocab/LibrarySystem" resource="http://link.library.missouri.edu/"><span property="name http://bibfra.me/vocab/lite/label"><a property="url" href="http://link.library.missouri.edu/">University of Missouri Libraries</a></span></span></span></span></div>
