{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T14:24:24Z","timestamp":1725978264963},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319105741"},{"type":"electronic","value":"9783319105758"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_5","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"153-171","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Explicit-State Model Checking"],"prefix":"10.1007","author":[{"given":"Gerard J.","family":"Holzmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"5_CR1","unstructured":"The game of tic-tac-toe. http:\/\/f2.org\/maths\/ttt.html"},{"issue":"4","key":"5_CR2","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/s100090050038","volume":"2","author":"G. Avrunin","year":"2000","unstructured":"Avrunin, G., Corbett, J., Dwyer, M., Pasareanu, C., Siegel, S.: Benchmarking finite-state verifiers. Int. J. Softw. Tools Technol. Transf. 2(4), 317\u2013320 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR3","series-title":"LNCS","first-page":"234","volume-title":"Intl. Symp. Automated Technology for Verification and Analysis (ATVA)","author":"J. Barnet","year":"2009","unstructured":"Barnet, J., Brim, L., Rockai, P.: DiVinE multi-core, a parallel LTL model checker. In: Liu, Z., Ravn, A.P. (eds.) Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol.\u00a05799, pp.\u00a0234\u2013239. Springer, Heidelberg (2009)"},{"issue":"7","key":"5_CR4","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1145\/362686.362692","volume":"13","author":"B. Bloom","year":"1970","unstructured":"Bloom, B.: Spacetime trade-offs in hash coding with allowable errors. Commun. ACM 13(7), 422\u2013426 (1970)","journal-title":"Commun. ACM"},{"key":"5_CR5","unstructured":"Bosnacki, D.: Enhancing state space reduction techniques for model checking. Ph.D. thesis, Eindhoven University of Technology (2001)"},{"key":"5_CR6","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BFb0028741","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"E. Clarke","year":"1998","unstructured":"Clarke, E., Emerson, E., Jha, S., Sistla, A.: Symmetry reduction in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01427, pp.\u00a0147\u2013158. Springer, Heidelberg (1998)"},{"issue":"3","key":"5_CR7","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1109\/32.489078","volume":"22","author":"J. Corbett","year":"1996","unstructured":"Corbett, J.: Evaluating deadlock detection methods for concurrent software. Trans. Softw. Eng. 22(3), 161\u2013180 (1996)","journal-title":"Trans. Softw. Eng."},{"issue":"2\u20133","key":"5_CR8","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. Form. Methods Syst. Des. 1(2\u20133), 275\u2013288 (1992)","journal-title":"Form. Methods Syst. Des."},{"key":"5_CR9","volume-title":"Handbook of Model Checking","author":"D. Dams","year":"2018","unstructured":"Dams, D., Grumberg, O.: Abstraction and abstraction refinement. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"5_CR10","series-title":"LNCS","first-page":"153","volume-title":"Proc. 11th Intl. Conf. on Concurrency Theory (CONCUR)","author":"K. Etessami","year":"2000","unstructured":"Etessami, K., Holzmann, G.: Optimizing B\u00fcchi automata. In: Palamidessi, C. (ed.) Proc. 11th Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01877, pp.\u00a0153\u2013167. Springer, Heidelberg (2000)"},{"key":"5_CR11","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-0-387-34892-6_1","volume-title":"Proc. of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV","author":"R. Gerth","year":"1996","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Proc. of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification XV, pp.\u00a03\u201318. Chapman & Hall, London (1996)"},{"key":"5_CR12","first-page":"749","volume-title":"Intl. Conf. on Computer Communication (ICCC)","author":"J. Hajek","year":"1978","unstructured":"Hajek, J.: Automatically verified data transfer protocols. In: Intl. Conf. on Computer Communication (ICCC), pp.\u00a0749\u2013756 (1978)"},{"key":"5_CR13","unstructured":"Holzmann, G.: PAN: a protocol specification analyzer. Tech. Rep. TM81-11271-5, AT&T Bell Laboratories, (1981)"},{"issue":"2","key":"5_CR14","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1002\/spe.4380180203","volume":"18","author":"G. Holzmann","year":"1988","unstructured":"Holzmann, G.: An improved reachability analysis technique. Softw. Pract. Exp. 18(2), 137\u2013161 (1988)","journal-title":"Softw. Pract. Exp."},{"key":"5_CR15","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G. Holzmann","year":"2004","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"key":"5_CR16","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-31759-0_12","volume-title":"Intl. Workshop on Model Checking Software (SPIN)","author":"G. Holzmann","year":"2012","unstructured":"Holzmann, G.: Parallelizing the Spin model checker. In: Donaldson, A.F., Parker, D. (eds.) Intl. Workshop on Model Checking Software (SPIN). LNCS, vol.\u00a07385, pp.\u00a0155\u2013171. Springer, Heidelberg (2012)"},{"key":"5_CR17","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-642-39176-7_2","volume-title":"Intl. Symposium on Model Checking of Software (SPIN)","author":"G. Holzmann","year":"2013","unstructured":"Holzmann, G.: Proving properties of concurrent programs. In: Bartocci, E., Ramakrishnan, C.R. (eds.) Intl. Symposium on Model Checking of Software (SPIN). LNCS, vol.\u00a07976, pp.\u00a018\u201323. Springer, Heidelberg (2013)"},{"issue":"10","key":"5_CR18","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"G. Holzmann","year":"2007","unstructured":"Holzmann, G., Bosnacki, D.: The design of a multi-core extension of the Spin model checker. Trans. Softw. Eng. 33(10), 659\u2013674 (2007)","journal-title":"Trans. Softw. Eng."},{"issue":"3","key":"5_CR19","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/s00165-010-0160-5","volume":"23","author":"G. Holzmann","year":"2011","unstructured":"Holzmann, G., Florian, M.: Model checking with bounded context switching. Form. Asp. Comput. 23(3), 365\u2013389 (2011)","journal-title":"Form. Asp. Comput."},{"issue":"6","key":"5_CR20","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1109\/TSE.2010.110","volume":"37","author":"G. Holzmann","year":"2011","unstructured":"Holzmann, G., Joshi, R., Gorce, A.: Swarm verification techniques. Trans. Softw. Eng. 37(6), 845\u2013857 (2011)","journal-title":"Trans. Softw. Eng."},{"key":"5_CR21","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-0-387-34878-0_13","volume-title":"Proc. of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII","author":"G. Holzmann","year":"1995","unstructured":"Holzmann, G., Peled, D.: An improvement in formal verification. In: Proc. of the 7th IFIP WG6.1 International Conference on Formal Description Techniques VII, pp.\u00a0197\u2013211. Chapman & Hall, London (1995)"},{"key":"5_CR22","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1090\/dimacs\/032\/03","volume-title":"The Spin Verification System","author":"G. Holzmann","year":"1996","unstructured":"Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search. In: Gr\u00e9goire, J.C., Holzmann, G., Peled, D. (eds.) The Spin Verification System. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a032, pp.\u00a023\u201332. DIMACS\/AMS, Providence (1996)"},{"issue":"1\u20132","key":"5_CR23","first-page":"41","volume":"9","author":"C. Ip","year":"2006","unstructured":"Ip, C., Dill, D.: Better verification through symmetry. Form. Methods Syst. Des. 9(1\u20132), 41\u201375 (2006)","journal-title":"Form. Methods Syst. Des."},{"key":"5_CR24","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"GI-Conference on Theoretical Computer Science","author":"D. Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-Conference on Theoretical Computer Science. LNCS, vol.\u00a0104, pp.\u00a0167\u2013183. Springer, Heidelberg (1981)"},{"key":"5_CR25","volume-title":"Handbook of Model Checking","author":"D. Peled","year":"2018","unstructured":"Peled, D.: Partial-order reduction. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"5_CR26","first-page":"46","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a046\u201357. IEEE, Piscataway (1977)"},{"key":"5_CR27","volume-title":"Computer Networks","author":"A. Tanenbaum","year":"1981","unstructured":"Tanenbaum, A.: Computer Networks, 1st edn. Prentice Hall, New York (1981)","edition":"1"},{"issue":"1","key":"5_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M. Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994). Journal version of a conference paper first published in 1983","journal-title":"Inf. Comput."},{"issue":"3","key":"5_CR29","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1147\/rd.224.0393","volume":"22","author":"C. West","year":"1978","unstructured":"West, C.: General technique for communications protocol validation. IBM J. Res. Dev. 22(3), 393\u2013404 (1978)","journal-title":"IBM J. Res. Dev."},{"issue":"1","key":"5_CR30","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1147\/rd.221.0060","volume":"22","author":"C. West","year":"1978","unstructured":"West, C., Zafiropulo, P.: Automated validation of a communications protocol: the CCITT X.21 recommendation. IBM J. Res. Dev. 22(1), 60\u201371 (1978)","journal-title":"IBM J. Res. Dev."},{"key":"5_CR31","first-page":"184","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"P. Wolper","year":"1986","unstructured":"Wolper, P.: Specifying interesting properties of programs in propositional temporal logic. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0184\u2013193. ACM, New York (1986)"},{"key":"5_CR32","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/3-540-56922-7_6","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"P. Wolper","year":"1993","unstructured":"Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Courcoubetis, C. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0697, pp.\u00a059\u201370. Springer, Heidelberg (1993)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T05:44:10Z","timestamp":1571377450000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_5","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}