{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:20:23Z","timestamp":1759033223717},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,2,3]],"date-time":"2010-02-03T00:00:00Z","timestamp":1265155200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2010,5]]},"DOI":"10.1007\/s10009-010-0136-z","type":"journal-article","created":{"date-parts":[[2010,2,2]],"date-time":"2010-02-02T16:14:19Z","timestamp":1265127259000},"page":"139-153","source":"Crossref","is-referenced-by-count":13,"title":["Scalable shared memory LTL model checking"],"prefix":"10.1007","volume":"12","author":[{"given":"J.","family":"Barnat","sequence":"first","affiliation":[]},{"given":"L.","family":"Brim","sequence":"additional","affiliation":[]},{"given":"P.","family":"Ro\u010dkai","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,2,3]]},"reference":[{"key":"136_CR1","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: Parallel breadth-first search LTL model-checking. In: IEEE International Conference on Automated Software Engineering (ASE\u201903), pp. 106\u2013115. IEEE Computer Society Press (2003)","DOI":"10.1109\/ASE.2003.1240299"},{"key":"136_CR2","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: Scalable multi-core LTL model-checkin. In: Model Checking Software (SPIN\u201907), volume 4595 of LNCS, pp. 187\u2013203. Springer (2007)","DOI":"10.1007\/978-3-540-73370-6_13"},{"key":"136_CR3","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: DiVinE multi-core\u2014a parallel LTL model-checker. In: Automated Technology for Verification and Analysis (ATVA\u201908), volume 5311 of LNCS, pp. 234\u2013239. Springer (2008)","DOI":"10.1007\/978-3-540-88387-6_20"},{"key":"136_CR4","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., St\u0159 \u00edbrn\u00e1, J.: Distributed LTL model-checking in SPIN. In: Model Checking Software (SPIN\u201901), volume 2057 of LNCS, pp. 200\u2013216. Springer (2001)","DOI":"10.1007\/3-540-45139-0_13"},{"key":"136_CR5","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I.: Property driven distribution of nested DFS. In: International Workshop on Verification and Computational Logic (VCL\u201902), pp. 1\u201310. University of Southampton, UK. Technical Report DSSE-TR-2002-5 in DSSE (2002)"},{"key":"136_CR6","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I.: Cluster-based LTL model checking of large systems. In: Formal Methods for Components and Objects (FMCO\u201905), number 4111 in LNCS, pp. 259\u2013279. Springer (2006)","DOI":"10.1007\/11804192_13"},{"key":"136_CR7","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., Moravec, P., Ro\u010dkai, P., \u0160ime\u010dek, P.: DiVinE\u2014a tool for distributed verification (Tool Paper). In: Computer Aided Verification (CAV\u201906), volume 4144 of LNCS, pp. 278\u2013281. Springer (2006)","DOI":"10.1007\/11817963_26"},{"key":"136_CR8","unstructured":"Barnat, J., Ro\u010dkai, P.: Shared hash tables in parallel model checking. In: Parallel and Distributed Methods in verification (PDMC\u201907), pp. 81\u201395. CTIT, University of Twente (2007)"},{"key":"136_CR9","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Hune, T.S., Vaandrager, F.W.: Distributed timed model checking\u2014How the search order matters. In: Computer Aided Verification (CAV\u201900), volume 1855 of LNCS, pp. 216\u2013231. Springer (2000)","DOI":"10.1007\/10722167_19"},{"issue":"1","key":"136_CR10","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s10009-003-0129-2","volume":"7","author":"A. Bell","year":"2005","unstructured":"Bell A., Haverkort B.R.: Sequential and distributed model checking of Petri Net specifications. Int. J. Softw. Tools Technol. Transfer 7(1), 43\u201360 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"136_CR11","doi-asserted-by":"crossref","unstructured":"Berger, E., McKinley, K., Blumofe, R., Wilson, P.: Hoard: a scalable memory allocator for multithreaded applications. In: International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-IX), pp. 117\u2013128. ACM Press (2000)","DOI":"10.1145\/378993.379232"},{"issue":"1","key":"136_CR12","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/s10009-004-0159-4","volume":"7","author":"S. Blom","year":"2005","unstructured":"Blom S., Orzan S.: A distributed algorithm for strong bisimulation reduction of state spaces. Int. J. Softw. Tools Technol. Transfer 7(1), 74\u201386 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"136_CR13","doi-asserted-by":"crossref","unstructured":"Bollig, B., Leucker, M., Weber, M.: Parallel model checking for the alternation free\u00a0\u03bc-calculus. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901), volume 2031 of LNCS, pp. 543\u2013558. Springer (2001)","DOI":"10.1007\/3-540-45319-9_37"},{"key":"136_CR14","doi-asserted-by":"crossref","unstructured":"Brim, L., \u010cern\u00e1, I., Moravec, P., \u0160im\u0161a, J.: Accepting predecessors are better than back edges in distributed LTL model-checking. In: Formal Methods in Computer-Aided Design (FMCAD\u201904), volume 3312 of LNCS, pp. 352\u2013366. Springer (2004)","DOI":"10.1007\/978-3-540-30494-4_25"},{"key":"136_CR15","doi-asserted-by":"crossref","unstructured":"Brim, L., \u010cern\u00e1, I., Kr\u010d\u00e1l, P., Pel\u00e1nek, R.: Distributed LTL model checking based on negative cycle detection. In: Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201901), volume 2245 of LNCS, pp. 96\u2013107. Springer (2001)","DOI":"10.1007\/3-540-45294-X_9"},{"issue":"2","key":"136_CR16","first-page":"3","volume":"132","author":"L. Brim","year":"2006","unstructured":"Brim L., \u010cern\u00e1 I., Moravec P., \u0160im\u0161a J.: How to order vertices for distributed LTL model-checking based on accepting predecessors. ENTCS 132(2), 3\u201318 (2006)","journal-title":"ENTCS"},{"key":"136_CR17","doi-asserted-by":"crossref","unstructured":"Caselli, S., Conte, G., Marenzoni, P.: Parallel state space exploration for GSPN models. In: Applications and Theory of Petri Nets (PN\u201995), volume 935 of LNCS, pp. 181\u2013200. Springer (1995)","DOI":"10.1007\/3-540-60029-9_40"},{"key":"136_CR18","doi-asserted-by":"crossref","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Distributed explicit fair cycle detection (set based approach). In: Model Checking Software (SPIN\u201903), volume 2648 of LNCS, pp. 49\u201373. Springer (2003)","DOI":"10.1007\/3-540-44829-2_4"},{"issue":"1","key":"136_CR19","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1287\/ijoc.10.1.82","volume":"10","author":"G. Ciardo","year":"1998","unstructured":"Ciardo G., Gluckman J., Nicol D.M.: Distributed state space generation of discrete-state +stochastic models. INFORMS J. Comput. 10(1), 82\u201393 (1998)","journal-title":"INFORMS J. Comput."},{"key":"136_CR20","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"Courcoubetis C., Vardi M.Y., Wolper P., Yannakakis M.: Memory-efficient algorithms for the verification of temporal properties. Formal Methods Syst. Des. 1, 275\u2013288 (1992)","journal-title":"Formal Methods Syst. Des."},{"key":"136_CR21","doi-asserted-by":"crossref","unstructured":"Fisler, K., Fraer, R., Kamhi, G., Vardi, M.Y., Yang, Z.: Is there a best symbolic cycle-detection algorithm? In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901), volume 2031 of LNCS, pp. 420\u2013434. Springer (2001)","DOI":"10.1007\/3-540-45319-9_29"},{"key":"136_CR22","doi-asserted-by":"crossref","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.: Parallel state space construction for model-checking. In: Model Checking Software (SPIN\u201901), volume 2057 of LNCS, pp. 217\u2013234. Springer (2001)","DOI":"10.1007\/3-540-45139-0_14"},{"issue":"1","key":"136_CR23","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1016\/j.tcs.2005.07.004","volume":"345","author":"J. Geldenhuys","year":"2005","unstructured":"Geldenhuys J., Valmari A.: More efficient on-the-fly LTL verification with Tarjan\u2019s algorithm. Theor. Comput. Sci. 345(1), 60\u201382 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"136_CR24","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1016\/j.tcs.2005.07.004","volume":"345","author":"J. Geldenhuys","year":"2005","unstructured":"Geldenhuys J., Valmari A.: More efficient on-the-fly LTL verification with Tarjan\u2019s algorithm. Theor. Comput. Sci. 345(1), 60\u201382 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"136_CR25","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Heyman, T., Ifergan, N., Schuster, A.: achieving speedups in distributed symbolic reachability analysis through asynchronous computation. In: Correct Hardware Design and Verification Methods (CHARME\u201905), volume 3725 of LNCS, pp. 129\u2013145. Springer (2005)","DOI":"10.1007\/11560548_12"},{"key":"136_CR26","doi-asserted-by":"crossref","unstructured":"Grumberg, O., Heyman, T., Schuster, A.: Distributed model checking for\u00a0\u03bc-calculus. In: Computer Aided Verification (CAV\u201901), volume 2102 of LNCS, pp. 350\u2013362. Springer (2001)","DOI":"10.1007\/3-540-44585-4_32"},{"key":"136_CR27","doi-asserted-by":"crossref","unstructured":"Haverkort, B.R., Bell, A., Bohnenkamp, H.C.: On the efficient sequential and distributed generation of very large Markov chains from stochastic Petri Nets. In: International Workshop on Petri Net and Performance Models (PNPM\u201999), pp. 12\u201321. IEEE Computer Society Press (1999)","DOI":"10.1109\/PNPM.1999.796528"},{"key":"136_CR28","volume-title":"The Spin Model Checker: Primer and Reference Manual","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, Reading (2003)"},{"issue":"10","key":"136_CR29","doi-asserted-by":"crossref","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"G.J. Holzmann","year":"2007","unstructured":"Holzmann G.J., Bosnacki 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":"136_CR30","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On nested depth first search. In: The SPIN Verification System, pp. 23\u201332. American Mathematical Society (1996)","DOI":"10.1090\/dimacs\/032\/03"},{"issue":"2","key":"136_CR31","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/s10703-006-0008-z","volume":"29","author":"C. Inggs","year":"2006","unstructured":"Inggs C., Barringer H.: CTL* model checking on a shared memory architecture. Formal Methods Syst. Des. 29(2), 135\u2013155 (2006)","journal-title":"Formal Methods Syst. Des."},{"key":"136_CR32","unstructured":"Lafuente, A.L.: Simplified distributed LTL model checking by localizing cycles. Technical Report 00176, Institut f\u00fcr Informatik, University Freiburg, Germany, July 2002"},{"issue":"5","key":"136_CR33","doi-asserted-by":"crossref","first-page":"538","DOI":"10.1109\/71.598280","volume":"8","author":"H.-F. Leung","year":"1997","unstructured":"Leung H.-F., Ting H.-F.: An optimal algorithm for global termination detection in shared-memory asynchronous multiprocessor systems. IEEE Trans. Parallel Distrib. Syst. 8(5), 538\u2013543 (1997)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"issue":"6","key":"136_CR34","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1145\/996893.996848","volume":"39","author":"M.M. Michael","year":"2004","unstructured":"Michael M.M.: Scalable lock-free dynamic memory allocation. SIGPLAN Not. 39(6), 35\u201346 (2004)","journal-title":"SIGPLAN Not."},{"key":"136_CR35","doi-asserted-by":"crossref","unstructured":"Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: Symposium on Principles of Distributed Computing (PODC\u201996), pp. 267\u2013275. ACM Press (1996)","DOI":"10.1145\/248052.248106"},{"key":"136_CR36","doi-asserted-by":"crossref","unstructured":"Pel\u00e1nek, R.: BEEM: benchmarks for explicit model checkers. In: Model Checking Software (SPIN\u201907), volume 4595 of LNCS, pp. 263\u2013267. Springer (2007)","DOI":"10.1007\/978-3-540-73370-6_17"},{"key":"136_CR37","doi-asserted-by":"crossref","unstructured":"Schwoon, S., Esparza, J.: A note on on-the-fly verification algorithms. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201905), volume 3440 of LNCS, pp. 174\u2013190. Springer (2005)","DOI":"10.1007\/978-3-540-31980-1_12"},{"key":"136_CR38","unstructured":"Talbot, S.: Performance tuning of programs for shared-memory multiprocessors. Master\u2019s thesis, Department of Computing, Imperial College, London (1995)"},{"key":"136_CR39","doi-asserted-by":"crossref","unstructured":"Tarjan, R.: Depth first search and linear graph algorithms. SIAM J. Comput. 2, 146\u2013160 (1972)","DOI":"10.1137\/0201010"},{"key":"136_CR40","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automata-theoretic model checking revisited. In: Verification, Model Checking, and Abstract Interpretation (VMCAI\u201907), volume 4349 of LNCS, pp. 137\u2013150. Springer (2007)","DOI":"10.1007\/978-3-540-69738-1_10"},{"key":"136_CR41","doi-asserted-by":"crossref","unstructured":"Verstoep, K., Bal, H., Barnat, J., Brim, L.: Efficient large-scale model checking. In: 23rd IEEE International Parallel & Distributed Processing Symposium (IPDPS 2009). IEEE (2009)","DOI":"10.1109\/IPDPS.2009.5161000"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0136-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0136-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0136-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:26Z","timestamp":1559114726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0136-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2,3]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["136"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0136-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2,3]]}}}