{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T13:22:15Z","timestamp":1765545735578},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614746"},{"type":"electronic","value":"9783540685999"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61474-5_85","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T16:41:20Z","timestamp":1330274480000},"page":"383-389","source":"Crossref","is-referenced-by-count":25,"title":["The state of Spin"],"prefix":"10.1007","author":[{"given":"Gerard J.","family":"Holzmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"33_CR1","unstructured":"C-T. Chou, D. Peled, Verifying a Model-Checking Algorithm, TACAS'96, Tools and Algorithms for the Construction and Analysis of Systems, Passau, Germany, March 1996."},{"key":"33_CR2","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal methods in system design 1 (1992) 275\u2013288.","journal-title":"Formal methods in system design"},{"issue":"8","key":"33_CR3","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E. Dijkstra","year":"1975","unstructured":"E. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Comm. ACM, 18(8), 1975, 453\u2013457.","journal-title":"Comm. ACM"},{"key":"33_CR4","first-page":"173","volume-title":"PSTV95, Protocol Specification Testing and Verification, Warsaw, Poland","author":"R. Gerth","year":"1995","unstructured":"R. Gerth, D. Peled, M.Y. Vardi, P. Wolper, Simple On-the-fly Automatic Verification of Linear Temporal Logic, PSTV95, Protocol Specification Testing and Verification, Warsaw, Poland. Chapman & Hall, Germany, 1995, 173\u2013184."},{"issue":"8","key":"33_CR5","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"C.A.R. Hoare, Communicating Sequential Processes, Comm. ACM, 21(8), 1978, 666\u2013677.","journal-title":"Comm. ACM"},{"issue":"No2","key":"33_CR6","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1002\/spe.4380180203","volume":"18","author":"G.J. Holzmann","year":"1988","unstructured":"G.J. Holzmann, An Improved Protocol Reachability Analysis Technique, Software Practice and Experience, Feb 1988, Vol 18, No 2, pp. 137\u2013161.","journal-title":"Software Practice and Experience"},{"key":"33_CR7","unstructured":"G.J. Holzmann, Design and Validation of Computer Protocols, Prentice Hall, 1992."},{"key":"33_CR8","unstructured":"G.J. Holzmann, D. Peled, An Improvement in Formal Verification, 7th Int. Conf. on Formal Description Techniques, Berne, Switzerland, 1994, 177\u2013194."},{"key":"33_CR9","first-page":"301","volume-title":"PSTV95, Protocol Specification Testing and Verification, Warsaw, Poland","author":"G.J. Holzmann","year":"1995","unstructured":"G.J. Holzmann, An Analysis of Bitstate Hashing, PSTV95, Protocol Specification Testing and Verification, Warsaw, Poland, Chapman & Hall, Germany, 1995, 301\u2013314."},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann, D. Peled, M. Yannakakis, On Nested Depth-First Search, In preparation, 1996.","DOI":"10.1090\/dimacs\/032\/03"},{"key":"33_CR11","unstructured":"B.W. Kernighan, D.M. Ritchie, The C programming Language, Prentice Hall, 1988."},{"key":"33_CR12","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan, Computer-Aided Verification of Coordinating Processes, Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"33_CR13","first-page":"377","volume-title":"LNCS 818","author":"D. Peled","year":"1994","unstructured":"D. Peled, Combining Partial Order Reductions with On-the-fly Model-Checking, Proc. CAV'94, 6th International Conference on Computer Aided Verification, LNCS 818, Springer-Verlag, 377\u2013390, 1994, Stanford CA, USA."},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"D. Peled, Partial Order Reduction: Model-Checking using Representatives, Proc. MFCS'96, 21st International Symposium on Mathamatical Foundations of Computer Science, September 1996, Cracow, Poland.","DOI":"10.1007\/3-540-61550-4_141"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"A. Pnueli, The temporal logic of programs, Proc. of the 18th IEEE Symp. on Foundation of Computer Science, 1977, 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"33_CR16","unstructured":"M.Y. Vardi, P. Wolper, An automata-theoretic approach to automatic program verification, Proc. of the 1st Symposium on Logic in Computer Science, 1986, Cambridge, England, 322\u2013331."},{"key":"33_CR17","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper, Temporal Logic Can be More Expressive, Information and Control 56 (1983), 72\u201399.","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61474-5_85.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T05:37:28Z","timestamp":1640929048000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_85"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_85","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}