{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:59:02Z","timestamp":1776333542905,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466803","type":"print"},{"value":"9783662466810","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46681-0_61","type":"book-chapter","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T18:56:36Z","timestamp":1427741796000},"page":"692-707","source":"Crossref","is-referenced-by-count":116,"title":["LTSmin: High-Performance Language-Independent Model Checking"],"prefix":"10.1007","author":[{"given":"Gijs","family":"Kant","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alfons","family":"Laarman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeroen","family":"Meijer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jaco","family":"van de Pol","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Blom","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom","family":"van Dijk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"61_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-642-10373-5_21","volume-title":"Formal Methods and Software Engineering","author":"J. Barnat","year":"2009","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol.\u00a05885, pp. 407\u2013425. Springer, Heidelberg (2009)"},{"key":"61_CR2","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: Parallel Partial Order Reduction with Topological Sort Proviso. In: SEFM 2010, pp. 222\u2013231. IEEE (2010)","DOI":"10.1109\/SEFM.2010.35"},{"key":"61_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"863","DOI":"10.1007\/978-3-642-39799-8_60","volume-title":"Computer Aided Verification","author":"J. Barnat","year":"2013","unstructured":"Barnat, J., et al.: DiVinE 3.0 \u2013 An Explicit-State Model Checker for Multithreaded C & C++ Programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 863\u2013868. Springer, Heidelberg (2013)"},{"key":"61_CR4","doi-asserted-by":"crossref","unstructured":"van der Berg, F.I., Laarman, A.W.: SpinS: Extending LTSmin with Promela through SpinJa. In: PDMC 2012. ENTCS, vol. 296, pp. 95\u2013105 (2013)","DOI":"10.1016\/j.entcs.2013.07.007"},{"key":"61_CR5","unstructured":"Blom, S.C.C., van de Pol, J.C., Weber, M.: Bridging the Gap between Enumerative and Symbolic Model Checkers. University of Twente (2009)"},{"issue":"1","key":"61_CR6","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1093\/logcom\/exp004","volume":"21","author":"S. Blom","year":"2009","unstructured":"Blom, S., Lisser, B., van de Pol, J., Weber, M.: A Database Approach to Distributed State-Space Generation. Journal of Logic and Computation\u00a021(1), 45\u201362 (2009)","journal-title":"Journal of Logic and Computation"},{"key":"61_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-540-85762-4_6","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"S. Blom","year":"2008","unstructured":"Blom, S., van de Pol, J.: Symbolic Reachability for Process Algebras with Recursive Data Types. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol.\u00a05160, pp. 81\u201395. Springer, Heidelberg (2008)"},{"key":"61_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-642-14295-6_31","volume-title":"Computer Aided Verification","author":"S.C.C. Blom","year":"2010","unstructured":"Blom, S.C.C., van de Pol, J.C., Weber, M.: LTSmin: Distributed and Symbolic Reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 354\u2013359. Springer, Heidelberg (2010)"},{"key":"61_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., et al.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"key":"61_CR10","doi-asserted-by":"crossref","unstructured":"Cleary, J.G.: Compact Hash Tables Using Bidirectional Linear Probing. IEEE Transactions on Computers C-33(9), 828\u2013834 (1984)","DOI":"10.1109\/TC.1984.1676499"},{"key":"61_CR11","doi-asserted-by":"crossref","unstructured":"Cranen, S., others: An Overview of the mCRL2 Toolset and Its Recent Advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 199\u2013213. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36742-7_15"},{"key":"61_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-33365-1_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"A.E. Dalsgaard","year":"2012","unstructured":"Dalsgaard, A.E., others: Multi-core Reachability for Timed Automata. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol.\u00a07595, pp. 91\u2013106. Springer, Heidelberg (2012)"},{"key":"61_CR13","unstructured":"Dam, M.: Translating CTL* into the modal \u03bc-calculus. Report ECS-LFCS-90-123, LFCS, University of Edinburgh (1990)"},{"key":"61_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/BFb0054180","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C. Daws","year":"1998","unstructured":"Daws, C., Tripakis, S.: Model checking of real-time reachability properties using abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 313\u2013329. Springer, Heidelberg (1998)"},{"key":"61_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-319-14313-2_18","volume-title":"Euro-Par 2014: Parallel Processing Workshops","author":"T. Dijk van","year":"2014","unstructured":"van Dijk, T., van de Pol, J.C.: Lace: non-blocking split deque for work-stealing. In: Lopes, L., et al. (eds.) Euro-Par 2014, Part II. LNCS, vol.\u00a08806, pp. 206\u2013217. Springer, Heidelberg (2014)"},{"key":"61_CR16","doi-asserted-by":"crossref","unstructured":"van Dijk, T., van\u00a0de Pol, J.C.: Sylvan: Multi-core Decision Diagrams. In: TACAS 2015. Springer (2015)","DOI":"10.1007\/978-3-662-46681-0_60"},{"key":"61_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-31980-1_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.A. Emerson","year":"2005","unstructured":"Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 382\u2013396. Springer, Heidelberg (2005)"},{"key":"61_CR18","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10009-010-0137-y","volume":"12","author":"S. Evangelista","year":"2010","unstructured":"Evangelista, S., Pajault, C.: Solving the Ignoring Problem for Partial Order Reduction. STTT\u00a012, 155\u2013170 (2010)","journal-title":"STTT"},{"key":"61_CR19","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., et al.: Improved Multi-core Nested Depth-First Search. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 269\u2013283. Springer, Heidelberg (2012)"},{"key":"61_CR20","unstructured":"Friedmann, O., Lange, M.: PGSolver (2008), \n                      \n                        https:\/\/github.com\/tcsprojects\/pgsolver"},{"key":"61_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0054165","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Garavel","year":"1998","unstructured":"Garavel, H.: OPEN\/C\u00c6SAR: An open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 68\u201384. Springer, Heidelberg (1998)"},{"issue":"2","key":"61_CR22","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","volume":"15","author":"H. Garavel","year":"2013","unstructured":"Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT\u00a015(2), 89\u2013107 (2013)","journal-title":"STTT"},{"key":"61_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"issue":"3","key":"61_CR24","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/j.scico.2004.08.002","volume":"56","author":"J.F. Groote","year":"2005","unstructured":"Groote, J.F., Willemse, T.A.C.: Model-checking processes with data. Science of Computer Programming\u00a056(3), 251\u2013273 (2005)","journal-title":"Science of Computer Programming"},{"key":"61_CR25","doi-asserted-by":"crossref","unstructured":"Guck, D., et al.: Analysis of Timed and Long-Run Objectives for Markov Automata. Logical Methods in Computer Science 10(3) (2014)","DOI":"10.2168\/LMCS-10(3:17)2014"},{"key":"61_CR26","first-page":"279","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE TSE\u00a023, 279\u2013295 (1997)","journal-title":"IEEE TSE"},{"key":"61_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-31759-0_12","volume-title":"Model Checking Software","author":"G.J. Holzmann","year":"2012","unstructured":"Holzmann, G.J.: Parallelizing the SPIN Model Checker. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol.\u00a07385, pp. 155\u2013171. Springer, Heidelberg (2012)"},{"key":"61_CR28","doi-asserted-by":"crossref","unstructured":"Howar, F., et al.: Rigorous examination of reactive systems. STTT 16(5) (2014)","DOI":"10.1007\/s10009-014-0337-y"},{"key":"61_CR29","doi-asserted-by":"crossref","unstructured":"Kant, G., van de Pol, J.: Generating and Solving Symbolic Parity Games. In: GRAPHITE 2014. EPTCS, vol. 159, pp. 2\u201314 (2014)","DOI":"10.4204\/EPTCS.159.2"},{"key":"61_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/BFb0013032","volume-title":"Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency","author":"S. Katz","year":"1989","unstructured":"Katz, S., Peled, D.: An efficient verification method for parallel and distributed programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. LNCS, vol.\u00a0354, pp. 489\u2013507. Springer, Heidelberg (1989)"},{"key":"61_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-38088-4_3","volume-title":"NASA Formal Methods","author":"A. Laarman","year":"2013","unstructured":"Laarman, A., Farag\u00f3, D.: Improved On-The-Fly Livelock Detection. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol.\u00a07871, pp. 32\u201347. Springer, Heidelberg (2013)"},{"key":"61_CR32","doi-asserted-by":"crossref","unstructured":"Laarman, A., Pater, E., van de Pol, J.C., Hansen, H.: Guard-based partial-order reduction. STTT (2014)","DOI":"10.1007\/978-3-642-39176-7_15"},{"key":"61_CR33","unstructured":"Laarman, A., van de Pol, J., Weber, M.: Boosting Multi-Core Reachability Performance with Shared Hash Tables. In: FMCAD 2010, pp. 247\u2013255. IEEE (2010)"},{"key":"61_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 Workshops 2011. LNCS, vol.\u00a06823, pp. 38\u201356. Springer, Heidelberg (2011)"},{"key":"61_CR35","unstructured":"Laarman, A.: Scalable Multi-Core Model Checking. Ph.D. thesis, University of Twente (2014)"},{"key":"61_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"968","DOI":"10.1007\/978-3-642-39799-8_69","volume-title":"Computer Aided Verification","author":"A. Laarman","year":"2013","unstructured":"Laarman, A., Olesen, M.C., Dalsgaard, A.E., Larsen, K.G., van de Pol, J.: Multi-core Emptiness Checking of Timed B\u00fcchi Automata Using Inclusion Abstraction. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 968\u2013983. Springer, Heidelberg (2013)"},{"key":"61_CR37","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., van de 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.\u00a06617, pp. 506\u2013511. Springer, Heidelberg (2011)"},{"key":"61_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a08855, pp. 267\u2013283. Springer, Heidelberg (2014)"},{"key":"61_CR39","unstructured":"Mateescu, R.: Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus. In: VMCAI 1998 (1998)"},{"key":"61_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-319-13338-6_16","volume-title":"Hardware and Software: Verification and Testing","author":"J.J.G. Meijer","year":"2014","unstructured":"Meijer, J.J.G., Kant, G., van de Pol, J.C., Blom, S.C.C.: Read, Write and Copy Dependencies for Symbolic Model Checking. In: Yahav, E. (ed.) HVC 2014. LNCS, vol.\u00a08855, pp. 204\u2013219. Springer, Heidelberg (2014)"},{"issue":"5","key":"61_CR41","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s10009-014-0324-3","volume":"16","author":"J. Pol van de","year":"2014","unstructured":"van de Pol, J., Ruys, T.C., te Brinke, S.: Thoughtful brute-force attack of the RERS 2012 and 2013 Challenges. STTT\u00a016(5), 481\u2013491 (2014)","journal-title":"STTT"},{"key":"61_CR42","unstructured":"RERS \u2013 Rigorous Examination of Reactive Systems, \n                      \n                        http:\/\/rers-challenge.org\/"},{"key":"61_CR43","unstructured":"Timmer, M.: Efficient modelling, generation and analysis of Markov automata. Ph.D. thesis, University of Twente (2013)"},{"key":"61_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-51285-3_35","volume-title":"PARLE \u201989 - Parallel Architectures and Languages Europe","author":"A. Valmari","year":"1989","unstructured":"Valmari, A.: Eliminating Redundant Interleavings During Concurrent Program Verification. In: Odijk, E., Rem, M., Syre, J.-C. (eds.) PARLE 1989. LNCS, vol.\u00a0366, pp. 89\u2013103. Springer, Heidelberg (1989)"},{"key":"61_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-642-25929-6_18","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"S. Vegt van der","year":"2012","unstructured":"van der Vegt, S., Laarman, A.W.: A parallel compact hash table. In: Kot\u00e1sek, Z., Bouda, J., \u010cern\u00e1, I., Sekanina, L., Vojnar, T., Anto\u0161, D. (eds.) MEMICS 2011. LNCS, vol.\u00a07119, pp. 191\u2013204. Springer, Heidelberg (2012)"},{"issue":"1\u20132","key":"61_CR46","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W. Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees. Theoretical Computer Science\u00a0200(1\u20132), 135\u2013183 (1998)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46681-0_61","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T14:21:17Z","timestamp":1559139677000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46681-0_61"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466803","9783662466810"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}