{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:35:43Z","timestamp":1780115743144,"version":"3.54.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662491218","type":"print"},{"value":"9783662491225","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49122-5_15","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T00:01:36Z","timestamp":1450915296000},"page":"311-327","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Cloud-Based Verification of Concurrent Software"],"prefix":"10.1007","author":[{"given":"Gerard J.","family":"Holzmann","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"issue":"7","key":"15_CR1","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1145\/362686.362692","volume":"13","author":"BH Bloom","year":"1970","unstructured":"Bloom, B.H.: Space\/Time trade-offs in hash coding with allowable errors. Comm. ACM 13(7), 422\u2013426 (1970)","journal-title":"Comm. ACM"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/3-540-40026-5_4","volume-title":"Distributed Computing","author":"B Adsul","year":"2000","unstructured":"Adsul, B., Flood, C.H., Garthwaite, A.T., Martin, P.A., Shavit, N.N., Steele Jr., G.L.: Even better DCAS-based concurrent deques. In: Herlihy, M.P. (ed.) DISC 2000. LNCS, vol. 1914, pp. 59\u201373. Springer, Heidelberg (2000)"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Doherty, S., Detlefs, D.L., Groves, L., et al.: DCAS is not a silver bullet for nonblocking algorithm design. In: Gibbons, P.B., Adler, M. (eds.) Proceedings of Sixteenth Annual ACM Symposium on Parallel Algorithms, pp. 216\u2013224, Barcelona (2004)","DOI":"10.1145\/1007912.1007945"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Elbaum, S.G., et al.: Parallel randomized state-space search. In: Proceedings of ICSE 2007, pp. 3\u201312 (2007)","DOI":"10.21236\/ADA459092"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"Havelund, K.: Mechanical verification of a garbage collector. In: Proceedings of International Workshop on High-Level Parallel Programming Models and Supportive Environments, pp. 1258\u20131283, Puerto Rico (1999)","DOI":"10.1007\/BFb0098007"},{"key":"15_CR6","unstructured":"Holzmann, G.J.: On limits and possibilities of automated protocol analysis. In: Proceedings of 6th International Conference on Protocol Specification, Testing and Verification INWG IFIP, pp. 339\u2013344 (1987)"},{"issue":"2","key":"15_CR7","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1002\/bltj.2223","volume":"5","author":"GJ Holzmann","year":"2000","unstructured":"Holzmann, G.J., Smith, M.H.: Automating software feature verification. Bell Labs Tech. J. 5(2), 72\u201387 (2000). Special Issue on Software Complexity","journal-title":"Bell Labs Tech. J."},{"key":"15_CR8","volume-title":"The Spin Model Checker - Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"issue":"6","key":"15_CR9","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1109\/TSE.2010.110","volume":"37","author":"GJ Holzmann","year":"2011","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845\u2013857 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"15_CR10","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/s00165-010-0160-5","volume":"23","author":"GJ Holzmann","year":"2001","unstructured":"Holzmann, G.J., Florian, M.: Model checking with bounded context switching. Formal Aspects Comput. 23(3), 365\u2013389 (2001)","journal-title":"Formal Aspects Comput."},{"issue":"2","key":"15_CR11","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/2560217.2560218","volume":"57","author":"GJ Holzmann","year":"2014","unstructured":"Holzmann, G.J.: Mars code. Commun. ACM 57(2), 64\u201373 (2014)","journal-title":"Commun. ACM"},{"key":"15_CR12","unstructured":"Erratum to [11]. \n                      http:\/\/spinroot.com\/dcas\/"},{"issue":"2","key":"15_CR13","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/s00165-006-0022-3","volume":"19","author":"Rajeev Joshi","year":"2007","unstructured":"Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. In: Proceedings of Verified Software: Theories, Tools, Experiments, Formal Aspects of Computing, vol. 19(2), pp. 269\u2013272 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"15_CR14","unstructured":"Modex, a model extractor for C code. \n                      http:\/\/spinroot.com\/modex\/"},{"issue":"2","key":"15_CR15","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/s10703-005-1490-4","volume":"26","author":"J Penix","year":"2005","unstructured":"Penix, J., Visser, W., Pasareanu, C., et al.: Verifying time partitioning in the DEOS scheduling kernel. Formal Meth. Syst. Des. J. 26(2), 103\u2013135 (2005)","journal-title":"Formal Meth. Syst. Des. J."},{"key":"15_CR16","unstructured":"The logic model checker Spin. \n                      http:\/\/spinroot.com\/"},{"key":"15_CR17","unstructured":"The Fleet distributed system. \n                      https:\/\/github.com\/coreos\/fleet\/"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49122-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T00:34:34Z","timestamp":1559349274000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,25]]},"assertion":[{"value":"25 December 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}