{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:54:21Z","timestamp":1743119661308,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319490519"},{"type":"electronic","value":"9783319490526"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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-319-49052-6_2","type":"book-chapter","created":{"date-parts":[[2016,10,31]],"date-time":"2016-10-31T10:34:50Z","timestamp":1477910090000},"page":"18-33","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Multi-core SCC-Based LTL Model Checking"],"prefix":"10.1007","author":[{"given":"Vincent","family":"Bloemen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,11,1]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Blahoudek, F., Duret-Lutz, A., K\u0159et\u00ednsk\u00fd, M., Strej\u010dek, J.: Is there a best B\u00fcchi automaton for explicit model checking? In: Proceedings of the 2014 International SPIN Symposium on Model Checking of Software, SPIN 2014, pp. 68\u201376. ACM (2014)","DOI":"10.1145\/2632362.2632377"},{"key":"2_CR2","doi-asserted-by":"crossref","unstructured":"Bloemen, V., Laarman, A., van de Pol, J.: Multi-core on-the-fly SCC decomposition. In: Proceedings of the 21st ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP 2016, pp. 8:1\u20138:12. ACM (2016)","DOI":"10.1145\/3016078.2851161"},{"key":"2_CR3","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/3-540-56922-7","volume-title":"Computer-Aided Verification","author":"C Courcoubetis","year":"1993","unstructured":"Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-efficient algorithms for the verification of temporal properties. In: Kurshan, R. (ed.) Computer-Aided Verification, pp. 129\u2013142. Springer US, New York (1993)"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/3-540-48119-2_16","volume-title":"FM 1999 \u2014 Formal Methods","author":"J-M Couvreur","year":"1999","unstructured":"Couvreur, J.-M.: On-the-fly verification of linear temporal logic. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 253\u2013271. Springer, Heidelberg (1999). doi:\n                    10.1007\/3-540-48119-2_16"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/11537328_15","volume-title":"Model Checking Software","author":"J-M Couvreur","year":"2005","unstructured":"Couvreur, J.-M., Duret-Lutz, A., Poitrenaud, D.: On-the-fly emptiness checks for generalized B\u00fcchi automata. In: Godefroid, P. (ed.) SPIN 2005. LNCS, vol. 3639, pp. 169\u2013184. Springer, Heidelberg (2005). doi:\n                    10.1007\/11537328_15"},{"key":"2_CR6","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-1-4612-5695-3_3","volume-title":"Selected Writings on Computing: A personal Perspective","author":"EW Dijkstra","year":"1982","unstructured":"Dijkstra, E.W.: Finding the maximum strong components in a directed graph. In: Dijkstra, E.W. (ed.) Selected Writings on Computing: A personal Perspective. Texts and Monographs in Computer Science, pp. 22\u201330. Springer, New York (1982)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0 \u2014 a framework for LTL and \n                    \n                      \n                    \n                    $$\\omega $$\n                  -automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Heidelberg (2016). doi:\n                    10.1007\/978-3-319-46520-3_8"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-642-33386-6_22","volume-title":"Automated Technology for Verification and Analysis","author":"S Evangelista","year":"2012","unstructured":"Evangelista, S., Laarman, A., Petrucci, L., van de Pol, J.: Improved multi-core nested depth-first search. In: Chakraborty, S., Mukund, M. (eds.) Automated Technology for Verification and Analysis. LNCS, vol. 7561, pp. 269\u2013283. Springer, Heidelberg (2012)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-24372-1_27","volume-title":"Automated Technology for Verification and Analysis","author":"S Evangelista","year":"2011","unstructured":"Evangelista, S., Petrucci, L., Youcef, S.: Parallel nested depth-first searches for LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 381\u2013396. Springer, Heidelberg (2011). doi:\n                    10.1007\/978-3-642-24372-1_27"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/3-540-45591-4_68","volume-title":"Parallel and Distributed Processing","author":"LK Fleischer","year":"2000","unstructured":"Fleischer, L.K., Hendrickson, B., P\u0131nar, A.: On identifying strongly connected components in parallel. In: Rolim, J. (ed.) IPDPS 2000. LNCS, vol. 1800, pp. 505\u2013511. Springer, Heidelberg (2000). doi:\n                    10.1007\/3-540-45591-4_68"},{"key":"2_CR11","unstructured":"Gaiser, A., Schwoon, S.: Comparison of Algorithms for Checking Emptiness on B\u00fcchi Automata. CoRR abs\/0910.3766 (2009)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-540-24730-2_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Geldenhuys","year":"2004","unstructured":"Geldenhuys, J., Valmari, A.: Tarjan\u2019s algorithm makes on-the-fly LTL verification more efficient. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 2988, pp. 205\u2013219. Springer, Heidelberg (2004)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Sytems \u2014 FORTE 2002","author":"D Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: improving translation of LTL formulae to B\u00fcchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 308\u2013326. Springer, Heidelberg (2002). doi:\n                    10.1007\/3-540-36135-9_20"},{"issue":"6","key":"2_CR14","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., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845\u2013857 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2_CR15","unstructured":"Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search. In: Proceedings of the Second SPIN Workshop, vol. 32, pp. 81\u201389 (1996)"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Hong, S., Rodia, N., Olukotun, K.: On fast parallel detection of strongly connected components (SCC) in small-world graphs. In: 2013 International Conference High Performance Computing, Networking, Storage and Analysis (SC), pp. 1\u201311 (2013)","DOI":"10.1145\/2503210.2503246"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., Pol, J., Blom, S., Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). doi:\n                    10.1007\/978-3-662-46681-0_61"},{"key":"2_CR18","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Chiardo, G., Hamez, A., Jezequel, L., Miner, A., Meijer, J., Paviot-Adet, E., Racordon, D., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Trinh, G., Wolf, K.: Complete Results for the 2016 Edition of the Model Checking Contest (2016)"},{"key":"2_CR19","unstructured":"Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Linard, A., Beccuti, M., Hamez, A., Lopez-Bobeda, E., Jezequel, L., Meijer, J., Paviot-Adet, E., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Wolf, K.: Complete Results for the 2015 Edition of the Model Checking Contest (2015)"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-24372-1_23","volume-title":"Automated Technology for Verification and Analysis","author":"A Laarman","year":"2011","unstructured":"Laarman, A., Langerak, R., Pol, J., Weber, M., Wijs, A.: Multi-core nested depth-first search. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 321\u2013335. Springer, Heidelberg (2011). doi:\n                    10.1007\/978-3-642-24372-1_23"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Laarman, A., van de Pol, J.: Variations on multi-core nested depth-first search. In: Barnat, J., Heljanko, K. (eds.) PDMC 2011. EPTCS, vol. 72, pp. 13\u201328 (2011)","DOI":"10.4204\/EPTCS.72.2"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1007\/978-3-642-20398-5_40","volume-title":"NASA Formal Methods","author":"A Laarman","year":"2011","unstructured":"Laarman, A., Pol, J., Weber, M.: Multi-core LTSmin: marrying modularity and scalability. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 506\u2013511. Springer, Heidelberg (2011). doi:\n                    10.1007\/978-3-642-20398-5_40"},{"issue":"2","key":"2_CR23","first-page":"1","volume":"18","author":"G Lowe","year":"2015","unstructured":"Lowe, G.: Concurrent depth-first search algorithms based on Tarjan\u2019s algorithm. Int. J. Softw. Tools Technol. Transf. 18(2), 1\u201319 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, PODC 1987, p. 205. ACM (1987)","DOI":"10.1145\/41840.41857"},{"key":"2_CR25","unstructured":"Orzan, S.: On Distributed Verification and Verified Distribution. Ph.D. thesis (2004)"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: benchmarks for explicit model checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 263\u2013267. Springer, Heidelberg (2007). doi:\n                    10.1007\/978-3-540-73370-6_17"},{"issue":"5","key":"2_CR27","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/s10009-008-0070-5","volume":"10","author":"R Pel\u00e1nek","year":"2008","unstructured":"Pel\u00e1nek, R.: Properties of state spaces and their applications. Int. J. Softw. Tools Technol. Transf. 10(5), 443\u2013454 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-50517-2_79","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"VN Rao","year":"1988","unstructured":"Rao, V.N., Kumar, V.: Superlinear speedup in parallel state-space search. In: Nori, K.V., Kumar, S. (eds.) Foundations of Software Technology and Theoretical Computer Science. LNCS, vol. 338, pp. 161\u2013174. Springer, Heidelberg (1988)"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1007\/978-3-662-46681-0_56","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Renault","year":"2015","unstructured":"Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Parallel explicit model checking for generalized B\u00fcchi automata. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 613\u2013627. Springer, Heidelberg (2015). doi:\n                    10.1007\/978-3-662-46681-0_56"},{"key":"2_CR30","unstructured":"Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Variations on parallel explicit emptiness checks for generalized B\u00fcchi automata. Int. J. Softw. Tools Technol. Transf. 1\u201321 (2016). \n                    http:\/\/link.springer.com\/journal\/10009\/onlineFirst\/page\/1"},{"key":"2_CR31","doi-asserted-by":"crossref","unstructured":"Schudy, W.: Finding strongly connected components in parallel using O(log2n) reachability queries. In: Proceedings of the Twentieth Annual Symposium on Parallelism in Algorithms and Architectures, SPAA 2008, pp. 146\u2013151. ACM (2008)","DOI":"10.1145\/1378533.1378560"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-31980-1_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Schwoon","year":"2005","unstructured":"Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 174\u2013190. Springer, Heidelberg (2005). doi:\n                    10.1007\/978-3-540-31980-1_12"},{"key":"2_CR33","doi-asserted-by":"crossref","unstructured":"Slota, G.M., Rajamanickam, S., Madduri, K.: BFS and coloring-based parallel algorithms for strongly connected components and related problems. In: 2014 IEEE 28th International Parallel and Distributed Processing Symposium, pp. 550\u2013559 (2014)","DOI":"10.1109\/IPDPS.2014.64"},{"issue":"2","key":"2_CR34","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"RE Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"2_CR35","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the First Symposium on Logic in Computer Science, pp. 322\u2013331. IEEE Computer Society (1986)"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-540-45138-9_26","volume-title":"Mathematical Foundations of Computer Science 2003","author":"I \u010cern\u00e1","year":"2003","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Relating hierarchy of temporal properties to model checking. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol. 2747, pp. 318\u2013327. Springer, Heidelberg (2003). doi:\n                    10.1007\/978-3-540-45138-9_26"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-49052-6_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T01:22:08Z","timestamp":1558315328000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-49052-6_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319490519","9783319490526"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-49052-6_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"1 November 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"HVC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa Verification Conference","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 November 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 November 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"hvc2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}