Correct Hardware Design and Verification Methods (Record no. 187670)
[ view plain ]
| 000 -LEADER | |
|---|---|
| fixed length control field | 06778nam a22006615i 4500 |
| 001 - CONTROL NUMBER | |
| control field | 978-3-540-48153-9 |
| 003 - CONTROL NUMBER IDENTIFIER | |
| control field | DE-He213 |
| 005 - DATE AND TIME OF LATEST TRANSACTION | |
| control field | 20240423132429.0 |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION | |
| fixed length control field | cr nn 008mamaa |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION | |
| fixed length control field | 121227s1999 gw | s |||| 0|eng d |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER | |
| International Standard Book Number | 9783540481539 |
| -- | 978-3-540-48153-9 |
| 024 7# - OTHER STANDARD IDENTIFIER | |
| Standard number or code | 10.1007/3-540-48153-2 |
| Source of number or code | doi |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER | |
| Classification number | QA76.9.S88 |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | UYD |
| Source | bicssc |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | COM011000 |
| Source | bisacsh |
| 072 #7 - SUBJECT CATEGORY CODE | |
| Subject category code | UYD |
| Source | thema |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER | |
| Classification number | 004.2 |
| Edition number | 23 |
| 245 10 - TITLE STATEMENT | |
| Title | Correct Hardware Design and Verification Methods |
| Medium | [electronic resource] : |
| Remainder of title | 10th IFIP WG10.5 Advanced Research Working Conference, CHARME'99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings / |
| Statement of responsibility, etc | edited by Laurence Pierre, Thomas Kropf. |
| 250 ## - EDITION STATEMENT | |
| Edition statement | 1st ed. 1999. |
| 264 #1 - | |
| -- | Berlin, Heidelberg : |
| -- | Springer Berlin Heidelberg : |
| -- | Imprint: Springer, |
| -- | 1999. |
| 300 ## - PHYSICAL DESCRIPTION | |
| Extent | XII, 376 p. |
| Other physical details | online resource. |
| 336 ## - | |
| -- | text |
| -- | txt |
| -- | rdacontent |
| 337 ## - | |
| -- | computer |
| -- | c |
| -- | rdamedia |
| 338 ## - | |
| -- | online resource |
| -- | cr |
| -- | rdacarrier |
| 347 ## - | |
| -- | text file |
| -- | |
| -- | rda |
| 490 1# - SERIES STATEMENT | |
| Series statement | Lecture Notes in Computer Science, |
| International Standard Serial Number | 1611-3349 ; |
| Volume number/sequential designation | 1703 |
| 505 0# - FORMATTED CONTENTS NOTE | |
| Formatted contents note | Invited Talks -- Esterel and Jazz : Two Synchronous Languages for Circuit Design -- Design Process of Embedded Automotive Systems—Using Model Checking for Correct Specifications -- Proof of Microprocessors -- A Proof of Correctness of a Processor Implementing Tomasulo’s Algorithm without a Reorder Buffer -- Formal Verification of Explicitly Parallel Microprocessors -- Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic -- Model Checking -- Model Checking TLA+ Specifications -- Efficient Decompositional Model Checking for Regular Timing Diagrams -- Vacuity Detection in Temporal Model Checking -- Formal Methods and Industrial Applications -- Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard -- Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors -- Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics -- Abstraction and Compositional Techniques -- From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking -- Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction -- Abstract BDDs: A Technique for Using Abstraction in Model Checking -- Theorem Proving Related Approaches -- Formal Synthesis at the Algorithmic Level -- Xs Are for Trajectory Evaluation, Booleans Are for Theorem Proving -- Verification of Infinite State Systems by Compositional Model Checking -- Symbolic Simulation/Symbolic Traversal -- Formal Verification of Designs with Complex Control by Symbolic Simulation -- Hints to Accelerate Symbolic Traversal -- Specification Languages and Methodologies -- Modeling and Checking Networks of CommunicatingReal-Time Processes -- ”Have I Written Enough Properties?” - A Method of Comparison Between Specification and Implementation -- Program Slicing of Hardware Description Languages -- Posters -- Results of the Verification of a Complex Pipelined Machine Model -- Hazard—Freedom Checking in Speed—Independent Systems -- Yet Another Look at LTL Model Checking -- Verification of Finite-State-Machine Refinements Using a Symbolic Methodology -- Refinement and Property Checking in High-Level Synthesis Using Attribute Grammars -- A Systematic Incrementalization Technique and Its Application to Hardware Design -- Bisimulation and Model Checking -- Circular Compositional Reasoning about Liveness -- Symbolic Simulation of Microprocessor Models Using Type Classes in Haskell -- Exploiting Retiming in a Guided Simulation Based Validation Methodology -- Fault Models for Embedded Systems -- Validation of Object-Oriented Concurrent Designs by Model Checking. |
| 520 ## - SUMMARY, ETC. | |
| Summary, etc | CHARME’99 is the tenth in a series of working conferences devoted to the dev- opment and use of leading-edge formal techniques and tools for the design and veri?cation of hardware and systems. Previous conferences have been held in Darmstadt (1984), Edinburgh (1985), Grenoble (1986), Glasgow (1988), Leuven (1989), Torino (1991), Arles (1993), Frankfurt (1995) and Montreal (1997). This workshop and conference series has been organized in cooperation with IFIP WG 10. 5. It is now the biannual counterpart of FMCAD, which takes place every even-numbered year in the USA. The 1999 event took place in Bad Her- nalb, a resort village located in the Black Forest close to the city of Karlsruhe. The validation of functional and timing behavior is a major bottleneck in current VLSI design systems. A predominantly academic area of study until a few years ago, formal design and veri?cation techniques are now migrating into industrial use. The aim of CHARME’99 is to bring together researchers and users from academia and industry working in this active area of research. Two invited talks illustrate major current trends: the presentation by G´erard Berry (Ecole des Mines de Paris, Sophia-Antipolis, France) is concerned with the use of synchronous languages in circuit design, and the talk given by Peter Jansen (BMW, Munich, Germany) demonstrates an application of formal methods in an industrial environment. The program also includes 20 regular presentations and 12 short presentations/poster exhibitions that have been selected from the 48 submitted papers. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer systems. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer engineering. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer networks . |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computers. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer science. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Software engineering. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Dynamics. |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Nonlinear theories. |
| 650 14 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer System Implementation. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer Engineering and Networks. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer Hardware. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Computer Science Logic and Foundations of Programming. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Software Engineering. |
| 650 24 - SUBJECT ADDED ENTRY--TOPICAL TERM | |
| Topical term or geographic name as entry element | Applied Dynamical Systems. |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Pierre, Laurence. |
| Relator term | editor. |
| Relator code | edt |
| -- | http://id.loc.gov/vocabulary/relators/edt |
| 700 1# - ADDED ENTRY--PERSONAL NAME | |
| Personal name | Kropf, Thomas. |
| Relator term | editor. |
| Relator code | edt |
| -- | http://id.loc.gov/vocabulary/relators/edt |
| 710 2# - ADDED ENTRY--CORPORATE NAME | |
| Corporate name or jurisdiction name as entry element | SpringerLink (Online service) |
| 773 0# - HOST ITEM ENTRY | |
| Title | Springer Nature eBook |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Display text | Printed edition: |
| International Standard Book Number | 9783540665595 |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY | |
| Display text | Printed edition: |
| International Standard Book Number | 9783662197691 |
| 830 #0 - SERIES ADDED ENTRY--UNIFORM TITLE | |
| Uniform title | Lecture Notes in Computer Science, |
| -- | 1611-3349 ; |
| Volume number/sequential designation | 1703 |
| 856 40 - ELECTRONIC LOCATION AND ACCESS | |
| Uniform Resource Identifier | <a href="https://doi.org/10.1007/3-540-48153-2">https://doi.org/10.1007/3-540-48153-2</a> |
| 912 ## - | |
| -- | ZDB-2-SCS |
| 912 ## - | |
| -- | ZDB-2-SXCS |
| 912 ## - | |
| -- | ZDB-2-LNC |
| 912 ## - | |
| -- | ZDB-2-BAE |
| 942 ## - ADDED ENTRY ELEMENTS (KOHA) | |
| Koha item type | eBooks-CSE-Springer |
No items available.