The Resource Correct hardware design and verification methods : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings, Daniel Geist, Enrico Tronci, (eds.)
Correct hardware design and verification methods : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings, Daniel Geist, Enrico Tronci, (eds.)
Resource Information
The item Correct hardware design and verification methods : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings, Daniel Geist, Enrico Tronci, (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 : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings, Daniel Geist, Enrico Tronci, (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 12th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2003, held in L'Aquila, Italy in October 2003. The 24 revised full papers and 8 short papers presented were carefully reviewed and selected from 65 submissions. The papers are organized in topical sections on software verification, automata based methods, processor verification, specification methods, theorem proving, bounded model checking, and model checking and applications
- Language
- eng
- Extent
- 1 online resource (xii, 426 pages)
- Contents
-
- Invited Talks
- What Is beyond the RTL Horizon for Microprocessor and System Design?
- The Charme of Abstract Entities
- Tutorial
- The PSL/Sugar Specification Language A Language for all Seasons
- Software Verification
- Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular
- Predicate Abstraction with Minimum Predicates
- Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning
- Processor Verification
- Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP
- A Hazards-Based Correctness Statement for Pipelined Circuits
- Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT
- Automata Based Methods
- On Complementing Nondeterministic Büchi Automata
- Coverage Metrics for Formal Verification
- "More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking
- Short Papers 1
- An Optimized Symbolic Bounded Model Checking Engine
- Constrained Symbolic Simulation with Mathematica and ACL2
- Semi-formal Verification of Memory Systems by Symbolic Simulation
- CTL May Be Ambiguous When Model Checking Moore Machines
- Specification Methods
- Reasoning about GSTE Assertion Graphs
- Towards Diagrammability and Efficiency in Event Sequence Languages
- Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving
- Protocol Verification
- On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking
- On the Correctness of an Intrusion-Tolerant Group Communication Protocol
- Exact and Efficient Verification of Parameterized Cache Coherence Protocols
- Short Papers 2
- Design and Implementation of an Abstract Interpreter for VHDL
- A Programming Language Based Analysis of Operand Forwarding
- Integrating RAM and Disk Based Verification within the Mur? Verifier
- Design and Verification of CoreConnectTM IP Using Esterel
- Theorem Proving
- Inductive Assertions and Operational Semantics
- A Compositional Theory of Refinement for Branching Time
- Linear and Nonlinear Arithmetic in ACL2
- Bounded Model Checking
- Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking
- Convergence Testing in Term-Level Bounded Model Checking
- The ROBDD Size of Simple CNF Formulas
- Model Checking and Application
- Efficient Hybrid Reachability Analysis for Asynchronous Concurrent Systems
- Finite Horizon Analysis of Markov Chains with the Mur? Verifier
- Improved Symbolic Verification Using Partitioning Techniques
- Isbn
- 9783540397243
- Label
- Correct hardware design and verification methods : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings
- Title
- Correct hardware design and verification methods
- Title remainder
- 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings
- Statement of responsibility
- Daniel Geist, Enrico Tronci, (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 12th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2003, held in L'Aquila, Italy in October 2003. The 24 revised full papers and 8 short papers presented were carefully reviewed and selected from 65 submissions. The papers are organized in topical sections on software verification, automata based methods, processor verification, specification methods, theorem proving, bounded model checking, and model checking and applications
- Cataloging source
- COO
- Dewey number
- 621.39/5
- Illustrations
- illustrations
- Index
- index present
- LC call number
- TK7874.75
- LC item number
- .C453 2003
- Literary form
- non fiction
- http://bibfra.me/vocab/lite/meetingDate
- 2003
- http://bibfra.me/vocab/lite/meetingName
- CHARME 2003
- Nature of contents
-
- dictionaries
- bibliography
- http://library.link/vocab/relatedWorkOrContributorDate
-
- 1961-
- 1961-
- http://library.link/vocab/relatedWorkOrContributorName
-
- Geist, Daniel
- Tronci, Enrico
- Series statement
- Lecture notes in computer science,
- Series volume
- 2860
- http://library.link/vocab/subjectName
-
- Integrated circuits
- Integrated circuits
- Integrated circuits
- Integrated circuits
- Label
- Correct hardware design and verification methods : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings, Daniel Geist, Enrico Tronci, (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 Talks -- What Is beyond the RTL Horizon for Microprocessor and System Design? -- The Charme of Abstract Entities -- Tutorial -- The PSL/Sugar Specification Language A Language for all Seasons -- Software Verification -- Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular -- Predicate Abstraction with Minimum Predicates -- Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning -- Processor Verification -- Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP -- A Hazards-Based Correctness Statement for Pipelined Circuits -- Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT -- Automata Based Methods -- On Complementing Nondeterministic Büchi Automata -- Coverage Metrics for Formal Verification -- "More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking -- Short Papers 1 -- An Optimized Symbolic Bounded Model Checking Engine -- Constrained Symbolic Simulation with Mathematica and ACL2 -- Semi-formal Verification of Memory Systems by Symbolic Simulation -- CTL May Be Ambiguous When Model Checking Moore Machines -- Specification Methods -- Reasoning about GSTE Assertion Graphs -- Towards Diagrammability and Efficiency in Event Sequence Languages -- Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving -- Protocol Verification -- On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking -- On the Correctness of an Intrusion-Tolerant Group Communication Protocol -- Exact and Efficient Verification of Parameterized Cache Coherence Protocols -- Short Papers 2 -- Design and Implementation of an Abstract Interpreter for VHDL -- A Programming Language Based Analysis of Operand Forwarding -- Integrating RAM and Disk Based Verification within the Mur? Verifier -- Design and Verification of CoreConnectTM IP Using Esterel -- Theorem Proving -- Inductive Assertions and Operational Semantics -- A Compositional Theory of Refinement for Branching Time -- Linear and Nonlinear Arithmetic in ACL2 -- Bounded Model Checking -- Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking -- Convergence Testing in Term-Level Bounded Model Checking -- The ROBDD Size of Simple CNF Formulas -- Model Checking and Application -- Efficient Hybrid Reachability Analysis for Asynchronous Concurrent Systems -- Finite Horizon Analysis of Markov Chains with the Mur? Verifier -- Improved Symbolic Verification Using Partitioning Techniques
- Control code
- 53960348
- Dimensions
- unknown
- Extent
- 1 online resource (xii, 426 pages)
- Form of item
- online
- Isbn
- 9783540397243
- Lccn
- 2003057017
- Media category
- computer
- Media MARC source
- rdamedia
- Media type code
-
- c
- Other control number
- 10.1007/b93958
- Other physical details
- illustrations.
- Specific material designation
- remote
- System control number
- (OCoLC)53960348
- Label
- Correct hardware design and verification methods : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings, Daniel Geist, Enrico Tronci, (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 Talks -- What Is beyond the RTL Horizon for Microprocessor and System Design? -- The Charme of Abstract Entities -- Tutorial -- The PSL/Sugar Specification Language A Language for all Seasons -- Software Verification -- Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular -- Predicate Abstraction with Minimum Predicates -- Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning -- Processor Verification -- Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP -- A Hazards-Based Correctness Statement for Pipelined Circuits -- Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT -- Automata Based Methods -- On Complementing Nondeterministic Büchi Automata -- Coverage Metrics for Formal Verification -- "More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking -- Short Papers 1 -- An Optimized Symbolic Bounded Model Checking Engine -- Constrained Symbolic Simulation with Mathematica and ACL2 -- Semi-formal Verification of Memory Systems by Symbolic Simulation -- CTL May Be Ambiguous When Model Checking Moore Machines -- Specification Methods -- Reasoning about GSTE Assertion Graphs -- Towards Diagrammability and Efficiency in Event Sequence Languages -- Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving -- Protocol Verification -- On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking -- On the Correctness of an Intrusion-Tolerant Group Communication Protocol -- Exact and Efficient Verification of Parameterized Cache Coherence Protocols -- Short Papers 2 -- Design and Implementation of an Abstract Interpreter for VHDL -- A Programming Language Based Analysis of Operand Forwarding -- Integrating RAM and Disk Based Verification within the Mur? Verifier -- Design and Verification of CoreConnectTM IP Using Esterel -- Theorem Proving -- Inductive Assertions and Operational Semantics -- A Compositional Theory of Refinement for Branching Time -- Linear and Nonlinear Arithmetic in ACL2 -- Bounded Model Checking -- Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking -- Convergence Testing in Term-Level Bounded Model Checking -- The ROBDD Size of Simple CNF Formulas -- Model Checking and Application -- Efficient Hybrid Reachability Analysis for Asynchronous Concurrent Systems -- Finite Horizon Analysis of Markov Chains with the Mur? Verifier -- Improved Symbolic Verification Using Partitioning Techniques
- Control code
- 53960348
- Dimensions
- unknown
- Extent
- 1 online resource (xii, 426 pages)
- Form of item
- online
- Isbn
- 9783540397243
- Lccn
- 2003057017
- Media category
- computer
- Media MARC source
- rdamedia
- Media type code
-
- c
- Other control number
- 10.1007/b93958
- Other physical details
- illustrations.
- Specific material designation
- remote
- System control number
- (OCoLC)53960348
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/9D8X_KZDosY/" 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/9D8X_KZDosY/">Correct hardware design and verification methods : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings, Daniel Geist, Enrico Tronci, (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 : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings, Daniel Geist, Enrico Tronci, (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/9D8X_KZDosY/" 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/9D8X_KZDosY/">Correct hardware design and verification methods : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003 : proceedings, Daniel Geist, Enrico Tronci, (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>
