MARC details
| 000 -LEADER |
|---|
| fixed length control field |
05510cam a2200841 a 4500 |
| 001 - CONTROL NUMBER |
|---|
| control field |
ocm49568935 |
| 003 - CONTROL NUMBER IDENTIFIER |
|---|
| control field |
OCoLC |
| 005 - DATE AND TIME OF LATEST TRANSACTION |
|---|
| control field |
20240829153236.0 |
| 006 - FIXED-LENGTH DATA ELEMENTS--ADDITIONAL MATERIAL CHARACTERISTICS |
|---|
| fixed length control field |
m d |
| 007 - PHYSICAL DESCRIPTION FIXED FIELD--GENERAL INFORMATION |
|---|
| fixed length control field |
cr cn||||||||| |
| 008 - FIXED-LENGTH DATA ELEMENTS--GENERAL INFORMATION |
|---|
| fixed length control field |
011024s1999 maua ob 001 0 eng d |
| 010 ## - LIBRARY OF CONGRESS CONTROL NUMBER |
|---|
| LC control number |
99017979 |
| 040 ## - CATALOGING SOURCE |
|---|
| Original cataloging agency |
N$T |
| Language of cataloging |
eng |
| Description conventions |
pn |
| Transcribing agency |
N$T |
| Modifying agency |
OCLCQ |
| -- |
YDXCP |
| -- |
OCLCG |
| -- |
OCLCQ |
| -- |
TUU |
| -- |
OCLCQ |
| -- |
TNF |
| -- |
OCLCQ |
| -- |
ZCU |
| -- |
OCLCO |
| -- |
OCLCF |
| -- |
OCLCA |
| -- |
OCLCQ |
| -- |
NLGGC |
| -- |
OCLCQ |
| -- |
Z5A |
| -- |
CUY |
| -- |
OCLCQ |
| -- |
YDX |
| -- |
OCLCQ |
| -- |
OCLCO |
| -- |
WY@ |
| -- |
LUE |
| -- |
OCLCA |
| -- |
VTS |
| -- |
AGLDB |
| -- |
TOF |
| -- |
M8D |
| -- |
NOC |
| -- |
AU@ |
| -- |
UKSSU |
| -- |
UKAHL |
| -- |
OCLCA |
| -- |
OCLCO |
| -- |
OCLCQ |
| -- |
LDP |
| -- |
OCLCO |
| -- |
OCLCL |
| 015 ## - NATIONAL BIBLIOGRAPHY NUMBER |
|---|
| National bibliography number |
GB99V9765 |
| Source |
bnb |
| 016 7# - NATIONAL BIBLIOGRAPHIC AGENCY CONTROL NUMBER |
|---|
| Record control number |
000014472297 |
| Source |
AU |
| 019 ## - |
|---|
| -- |
1002297588 |
| -- |
1057970452 |
| -- |
1154977614 |
| -- |
1156942028 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
0585385580 |
| Qualifying information |
(electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9780585385587 |
| Qualifying information |
(electronic bk.) |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9780262270458 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
0262270455 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
0262292742 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9780262292740 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
0262032708 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| International Standard Book Number |
9780262032704 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
0262032708 |
| 020 ## - INTERNATIONAL STANDARD BOOK NUMBER |
|---|
| Canceled/invalid ISBN |
9780262032704 |
| 024 3# - OTHER STANDARD IDENTIFIER |
|---|
| Standard number or code |
9780262032704 |
| 035 ## - SYSTEM CONTROL NUMBER |
|---|
| System control number |
27235 |
| -- |
(N$T) |
| 035 ## - SYSTEM CONTROL NUMBER |
|---|
| System control number |
(OCoLC)49568935 |
| Canceled/invalid control number |
(OCoLC)1002297588 |
| -- |
(OCoLC)1057970452 |
| -- |
(OCoLC)1154977614 |
| -- |
(OCoLC)1156942028 |
| 050 #4 - LIBRARY OF CONGRESS CALL NUMBER |
|---|
| Classification number |
QA76.76.V47 |
| Item number |
C553 1999eb |
| 072 #7 - SUBJECT CATEGORY CODE |
|---|
| Subject category code |
COM |
| Subject category code subdivision |
051240 |
| Source |
bisacsh |
| 082 04 - DEWEY DECIMAL CLASSIFICATION NUMBER |
|---|
| Classification number |
004.2/1 |
| Edition number |
21 |
| 084 ## - OTHER CLASSIFICATION NUMBER |
|---|
| Classification number |
54.52 |
| Number source |
bcl |
| 049 ## - LOCAL HOLDINGS (OCLC) |
|---|
| Holding library |
MAIN |
| 100 1# - MAIN ENTRY--PERSONAL NAME |
|---|
| Personal name |
Clarke, Edmund M., |
| Titles and words associated with a name |
Jr. |
| Fuller form of name |
(Edmund Melson), |
| Dates associated with a name |
1945-2020, |
| Relator term |
author. |
| -- |
https://id.oclc.org/worldcat/entity/E39PBJxxh8wG8XjkGM3R3CDQbd |
| 9 (RLIN) |
931671 |
| 245 10 - TITLE STATEMENT |
|---|
| Title |
Model checking / |
| Statement of responsibility, etc. |
Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled. |
| 260 ## - PUBLICATION, DISTRIBUTION, ETC. (IMPRINT) |
|---|
| Place of publication, distribution, etc. |
Cambridge, Mass. : |
| Name of publisher, distributor, etc. |
MIT Press, |
| Date of publication, distribution, etc. |
©1999. |
| 300 ## - PHYSICAL DESCRIPTION |
|---|
| Extent |
1 online resource (xiv, 314 pages) : |
| Other physical details |
illustrations |
| 336 ## - CONTENT TYPE |
|---|
| Content type term |
text |
| Content type code |
txt |
| Source |
rdacontent |
| 337 ## - MEDIA TYPE |
|---|
| Media type term |
computer |
| Media type code |
c |
| Source |
rdamedia |
| 338 ## - CARRIER TYPE |
|---|
| Carrier type term |
online resource |
| Carrier type code |
cr |
| Source |
rdacarrier |
| 504 ## - BIBLIOGRAPHY, ETC. NOTE |
|---|
| Bibliography, etc |
Includes bibliographical references (pages 297-307) and index. |
| 588 0# - SOURCE OF DESCRIPTION NOTE |
|---|
| Source of description note |
Print version record. |
| 505 00 - FORMATTED CONTENTS NOTE |
|---|
| Title |
Modeling systems -- |
| -- |
Trmporal logics -- |
| -- |
Model checking -- |
| -- |
Binary decision diagram -- |
| -- |
Symbolic model checking -- |
| -- |
Model checking for the u-calculus -- |
| -- |
Model checking in practice -- |
| -- |
Model checking and automata theory -- |
| -- |
Partial order reduction -- |
| -- |
Equivalences and preorders between structures -- |
| -- |
Compositional reasoning -- |
| -- |
Abstraction -- |
| -- |
Symmetry -- |
| -- |
Infinite families of finite-state systems -- |
| -- |
Discrete real-time and quantitative temporal analysis -- |
| -- |
Continuous real time. |
| 520 8# - SUMMARY, ETC. |
|---|
| Summary, etc. |
Annotation. |
| Expansion of summary note |
Model checking is a technique for verifying finite state concurrent systems such as sequential circuit designs and communication protocols. It has a number of advantages over traditional approaches that are based on simulation, testing, and deductive reasoning. In particular, model checking is automatic and usually quite fast. Also, if the design contains an error, model checking will produce a counterexample that can be used to pinpoint the source of the error. The method, which was awarded the 1998 ACM Paris Kanellakis Award for Theory and Practice, has been used successfully in practice to verify real industrial designs, and companies are beginning to market commercial model checkers.<br /><br />The main challenge in model checking is dealing with the state space explosion problem. This problem occurs in systems with many components that can interact with each other or systems with data structures that can assume many different values. In such cases the number of global states can be enormous. Researchers have made considerable progress on this problem over the last ten years.<br /><br />This is the first comprehensive presentation of the theory and practice of model checking. The book, which includes basic as well as state-of-the-art techniques, algorithms, and tools, can be used both as an introduction to the subject and as a reference for researchers. |
| 546 ## - LANGUAGE NOTE |
|---|
| Language note |
English. |
| 590 ## - LOCAL NOTE (RLIN) |
|---|
| Local note |
Added to collection customer.56279.3 |
| 650 #0 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Computer systems |
| General subdivision |
Verification. |
| 9 (RLIN) |
1929 |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Logiciels |
| General subdivision |
Vérification. |
| 9 (RLIN) |
20690 |
| 650 #6 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Systèmes informatiques |
| General subdivision |
Vérification. |
| 9 (RLIN) |
967195 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
COMPUTERS |
| General subdivision |
Software Development & Engineering |
| -- |
Systems Analysis & Design. |
| Source of heading or term |
bisacsh |
| 9 (RLIN) |
19869 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Computer systems |
| General subdivision |
Verification |
| Source of heading or term |
fast |
| 9 (RLIN) |
1929 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Model Checking |
| Source of heading or term |
gnd |
| 9 (RLIN) |
1932 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Datenverarbeitungssystem |
| Source of heading or term |
gnd |
| 9 (RLIN) |
2952 |
| 650 17 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Computersystemen. |
| Source of heading or term |
gtt |
| 9 (RLIN) |
17288 |
| 650 17 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Modellen (theorie) |
| Authority record control number |
(NL-LeOCL)078593549 |
| Source of heading or term |
gtt |
| 9 (RLIN) |
230648 |
| 650 17 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Verificatie. |
| Authority record control number |
(NL-LeOCL)078940648 |
| Source of heading or term |
gtt |
| 9 (RLIN) |
17723 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Engineering & Applied Sciences. |
| Source of heading or term |
hilcc |
| 9 (RLIN) |
9023 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Computer Science. |
| Source of heading or term |
hilcc |
| 9 (RLIN) |
941 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Verificação e validação de software. |
| Source of heading or term |
larpcal |
| 9 (RLIN) |
283639 |
| 650 #7 - SUBJECT ADDED ENTRY--TOPICAL TERM |
|---|
| Topical term or geographic name as entry element |
Engenharia de software. |
| Source of heading or term |
larpcal |
| 9 (RLIN) |
283640 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Grumberg, Orna, |
| Relator term |
author. |
| 9 (RLIN) |
23510 |
| 700 1# - ADDED ENTRY--PERSONAL NAME |
|---|
| Personal name |
Peled, Doron A., |
| Dates associated with a name |
1962- |
| Relator term |
author. |
| -- |
https://id.oclc.org/worldcat/entity/E39PBJbCKd76vK9JBbkv3hrrMP |
| 9 (RLIN) |
17138 |
| 776 08 - ADDITIONAL PHYSICAL FORM ENTRY |
|---|
| Relationship information |
Print version: |
| Main entry heading |
Clarke, E.M., 1945- |
| Title |
Model checking. |
| Place, publisher, and date of publication |
Cambridge, Mass. : MIT Press, ©1999 |
| International Standard Book Number |
0262032708 |
| Record control number |
(DLC) 99017979 |
| -- |
(OCoLC)40675218 |
| 856 40 - ELECTRONIC LOCATION AND ACCESS |
|---|
| Materials specified |
EBSCOhost |
| Uniform Resource Identifier |
<a href="https://search.ebscohost.com/login.aspx?direct=true&scope=site&db=nlebk&db=nlabk&AN=27235">https://search.ebscohost.com/login.aspx?direct=true&scope=site&db=nlebk&db=nlabk&AN=27235</a> |
| 936 ## - OCLC/CONSER MISCELLANEOUS DATA (OCLC); PIECE USED FOR CATALOGING (pre-AACR2) (RLIN) |
|---|
| OCLC control number(s) of parallel record(s) (OCLC); Piece used for cataloging, PUC (RLIN) |
BATCHLOAD |
| 938 ## - |
|---|
| -- |
Askews and Holts Library Services |
| -- |
ASKH |
| -- |
AH37586296 |
| 938 ## - |
|---|
| -- |
EBSCOhost |
| -- |
EBSC |
| -- |
27235 |
| 938 ## - |
|---|
| -- |
YBP Library Services |
| -- |
YANK |
| -- |
2327219 |
| 938 ## - |
|---|
| -- |
YBP Library Services |
| -- |
YANK |
| -- |
10845174 |
| 938 ## - |
|---|
| -- |
Internet Archive |
| -- |
INAR |
| -- |
modelchecking0000clar |
| 994 ## - |
|---|
| -- |
92 |
| -- |
N$T |