{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:49Z","timestamp":1725663889286},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581796"},{"type":"electronic","value":"9783540484691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_54","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:24:59Z","timestamp":1330251899000},"page":"194-206","source":"Crossref","is-referenced-by-count":3,"title":["Modeling and verification of a real life protocol using symbolic model checking"],"prefix":"10.1007","author":[{"given":"Vivek G.","family":"Naik","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. P.","family":"Sistla","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"16_CR1","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D.L. Dill, \u201cSymbolic Modelchecking: 1020 states and beyond\u201d, In Proceedings of fifth annual Symposium on Logic in Computer Science, June 1990."},{"key":"16_CR2","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"2","author":"E. M. Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson and A. P. Sistla. \u201cAutomatic verification of finite-state concurrent systems using temporal logic.\u201d ACM Trans. Program. Lang. Syst. 8, 2, (April 1986), 244\u2013263.","journal-title":"ACM Trans. Program. Lang. Syst. 8"},{"key":"16_CR3","unstructured":"E. M. Clarke, J. R. Burch, O. Grumberg, D. E. Long and K. L. McMillan. \u201cAutomatic verification of Sequential Circuit Designs.\u201d Royal Society of London, October 1991."},{"key":"16_CR4","doi-asserted-by":"crossref","first-page":"1334","DOI":"10.1109\/PROC.1983.12775","volume":"71","author":"J. D. Day","year":"1983","unstructured":"J. D. Day and H. Zimmerman. \u201cThe OSI reference model.\u201d In Proc. of IEEE, volume 71, pages 1334\u20131340, December 1983.","journal-title":"Proc. of IEEE"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. \u201cChecking that finite state concurrent programs satisfy their linear specification.\u201d In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985.","DOI":"10.1145\/318593.318622"},{"key":"16_CR6","unstructured":"K. McMillan and J. Schawalbe. \u201cFormal verification of the Encore Gigamax cache consistency protocol.\u201d In International Symposium on Shared Memory Multiprocessors., 1991."},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. \u201cThe SMV system \u201d February 1992.","DOI":"10.1007\/978-1-4615-3190-6_4"},{"key":"16_CR8","unstructured":"K.L. McMillan. \u201cSymbolic Modelchecking: An approach to state explosion problem\u201d Ph.D. thesis, CMU-CS-92-131, may 1992."},{"key":"16_CR9","unstructured":"A. Tanenbaum. Computer Networks. Prentice Hall, 2nd edition, 1989."},{"key":"16_CR10","volume-title":"Information Processing Systems-Local Area Networks-Part3: Carrier sense multiple access with collision detection (CSMA\/CD) access method and physical layer specifications","author":"ANSI\/IEEE std","year":"1991","unstructured":"ANSI\/IEEE std. Information Processing Systems-Local Area Networks-Part3: Carrier sense multiple access with collision detection (CSMA\/CD) access method and physical layer specifications. The IEEE, Inc., NY, October 1991."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"H. B. Weinberg and L. D. Zuck. \u201cTimed Ethernet: Real-Time Formal Specification of Ethernet\u201d In Proc. 3rd CONCUR, August 1992.","DOI":"10.1007\/BFb0084804"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_54.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:17:54Z","timestamp":1605629874000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_54","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}