{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T16:57:23Z","timestamp":1761929843444},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319465197"},{"type":"electronic","value":"9783319465203"}],"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":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-46520-3_23","type":"book-chapter","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T10:40:27Z","timestamp":1474454427000},"page":"357-374","source":"Crossref","is-referenced-by-count":19,"title":["Partial-Order Reduction for GPU Model Checking"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Neele","sequence":"first","affiliation":[]},{"given":"Anton","family":"Wijs","sequence":"additional","affiliation":[]},{"given":"Dragan","family":"Bo\u0161na\u010dki","sequence":"additional","affiliation":[]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,22]]},"reference":[{"key":"23_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"9","key":"23_CR2","doi-asserted-by":"crossref","first-page":"1083","DOI":"10.1016\/j.jpdc.2011.10.015","volume":"72","author":"J Barnat","year":"2012","unstructured":"Barnat, J., Bauch, P., Brim, L., \u010ce\u0161ka, M.: Designing fast LTL model checking algorithms for many-core GPUs. J. Parallel Distrib. Comput. 72(9), 1083\u20131097 (2012)","journal-title":"J. Parallel Distrib. Comput."},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1007\/978-3-540-88387-6_20","volume-title":"Automated Technology for Verification and Analysis","author":"J Barnat","year":"2008","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: DiVinE multi-core \u2013 a parallel LTL model-checker. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 234\u2013239. Springer, Heidelberg (2008)"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: Parallel partial order reduction with topological sort proviso. In: Proceedings of the 8th IEEE International Conference on Software Engineering and Formal Methods, pp. 222\u2013231. IEEE (2010)","DOI":"10.1109\/SEFM.2010.35"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Defrancisco, R., Smolka, S.A.: Towards a GPGPU-parallel SPIN model checker. In: Proceedings of SPIN 2014, pp. 87\u201396. ACM, San Jose (2014)","DOI":"10.1145\/2632362.2632379"},{"issue":"4","key":"23_CR6","first-page":"365","volume":"11","author":"T Basten","year":"2004","unstructured":"Basten, T., Bo\u0161na\u010dki, D., Geilen, M.: Cluster-based partial-order reduction. Proc. ASE 11(4), 365\u2013402 (2004)","journal-title":"Proc. ASE"},{"issue":"1","key":"23_CR7","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/s10009-010-0176-4","volume":"13","author":"D Bo\u0161na\u010dki","year":"2010","unstructured":"Bo\u0161na\u010dki, D., Edelkamp, S., Sulewski, D., Wijs, A.: Parallel probabilistic model checking on general purpose graphics processors. STTT 13(1), 21\u201335 (2010)","journal-title":"STTT"},{"issue":"1","key":"23_CR8","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/s10009-008-0093-y","volume":"11","author":"D Bo\u0161na\u010dki","year":"2009","unstructured":"Bo\u0161na\u010dki, D., Leue, S., Lluch-Lafuente, A.: Partial-order reduction for general state exploring algorithms. STTT 11(1), 39\u201351 (2009)","journal-title":"STTT"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1007\/978-3-662-49674-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M \u010ce\u0161ka","year":"2016","unstructured":"\u010ce\u0161ka, M., Pila\u0159, P., Paoletti, N., Brim, L., Kwiatkowska, M.: PRISM-PSY: precise GPU-accelerated parameter synthesis for stochastic systems. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 367\u2013384. Springer, Heidelberg (2016)"},{"key":"23_CR10","doi-asserted-by":"crossref","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/978-3-642-33365-1_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"AE Dalsgaard","year":"2012","unstructured":"Dalsgaard, A.E., Laarman, A., Larsen, K.G., Olesen, M.C., van de Pol, J.: Multi-core reachability for timed automata. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 91\u2013106. Springer, Heidelberg (2012)"},{"key":"23_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/978-3-642-16164-3_8","volume-title":"Model Checking Software","author":"S Edelkamp","year":"2010","unstructured":"Edelkamp, S., Sulewski, D.: Efficient explicit-state model checking on general purpose graphics processors. In: van de Pol, J., Weber, M. (eds.) Model Checking Software. LNCS, vol. 6349, pp. 106\u2013123. Springer, Heidelberg (2010)"},{"issue":"2","key":"23_CR13","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1006\/inco.1994.1035","volume":"110","author":"P Godefroid","year":"1994","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. Inf. Comput. 110(2), 305\u2013326 (1994)","journal-title":"Inf. Comput."},{"issue":"10","key":"23_CR14","doi-asserted-by":"crossref","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"GJ Holzmann","year":"2007","unstructured":"Holzmann, G.J., Bo\u0161na\u010dki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Softw. Eng. 33(10), 659\u2013674 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"23_CR15","series-title":"FIP Advances in Information and Communication Technology","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-0-387-34878-0_13","volume-title":"Formal Description Techniques VII","author":"GJ Holzmann","year":"1995","unstructured":"Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Hogrefe, D., Leue, S. (eds.) Formal Description Techniques VII. FIP Advances in Information and Communication Technology, pp. 197\u2013211. Springer, New York (1995)"},{"key":"23_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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., van de Pol, J., Blom, S., van 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)"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1007\/978-3-642-39176-7_15","volume-title":"Model Checking Software","author":"A Laarman","year":"2013","unstructured":"Laarman, A., Pater, E., van de Pol, J., Weber, M.: Guard-based partial-order reduction. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 227\u2013245. Springer, Heidelberg (2013)"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1007\/978-3-642-22306-8_4","volume-title":"Model Checking Software","author":"A Laarman","year":"2011","unstructured":"Laarman, A., van de Pol, J., Weber, M.: Parallel recursive state compression for free. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol. 6823, pp. 38\u201356. Springer, Heidelberg (2011)"},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/978-3-319-13338-6_20","volume-title":"Hardware and Software: Verification and Testing","author":"A Laarman","year":"2014","unstructured":"Laarman, A., Wijs, A.: Partial-order reduction for multi-core LTL model checking. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 267\u2013283. Springer, Heidelberg (2014)"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1007\/11589976_6","volume-title":"Integrated Formal Methods","author":"F Lang","year":"2005","unstructured":"Lang, F.: Exp.Open 2.0: a flexible tool integrating partial order, compositional, and on-the-fly verification methods. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol. 3771, pp. 70\u201388. Springer, Heidelberg (2005)"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/3-540-56922-7_34","volume-title":"Computer Aided Verification","author":"D Peled","year":"1993","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409\u2013423. Springer, Heidelberg (1993)"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/BFb0023729","volume-title":"Computer-Aided Verification","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds.) Computer-Aided Verification. LNCS, vol. 531, pp. 156\u2013165. Springer, Heidelberg (1991)"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/3-540-53863-1_36","volume-title":"Advances in Petri Nets 1990","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990. LNCS, vol. 483, pp. 491\u2013515. Springer, Heidelberg (1991)"},{"key":"23_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1007\/978-3-319-41540-6_26","volume-title":"Computer Aided Verification","author":"A Wijs","year":"2016","unstructured":"Wijs, A.: BFS-based model checking of linear-time properties with an application on GPUs. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 472\u2013493. Springer, Heidelberg (2016)"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/978-3-642-31759-0_9","volume-title":"Model Checking Software","author":"AJ Wijs","year":"2012","unstructured":"Wijs, A.J., Bo\u0161na\u010dki, D.: Improving GPU sparse matrix-vector multiplication for probabilistic model checking. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 98\u2013116. Springer, Heidelberg (2012)"},{"key":"23_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-642-54862-8_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Wijs","year":"2014","unstructured":"Wijs, A., Bo\u0161na\u010dki, D.: GPUexplore: many-core on-the-fly state space exploration using GPUs. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 233\u2013247. Springer, Heidelberg (2014)"},{"issue":"2","key":"23_CR27","first-page":"1","volume":"18","author":"A Wijs","year":"2015","unstructured":"Wijs, A., Bo\u0161na\u010dki, D.: Many-core on-the-fly model checking of safety properties using GPUs. STTT 18(2), 1\u201317 (2015)","journal-title":"STTT"},{"key":"23_CR28","doi-asserted-by":"crossref","unstructured":"Wu, Z., Liu, Y., Sun, J., Shi, J., Qin, S.: GPU accelerated on-the-fly reachability checking. In: Proceedings of the 20th International Conference on Engineering of Complex Computer Systems, pp. 100\u2013109. IEEE (2015)","DOI":"10.1109\/ICECCS.2015.21"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-46520-3_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T23:19:52Z","timestamp":1498346392000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-46520-3_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319465197","9783319465203"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-46520-3_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}