{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T08:42:57Z","timestamp":1780562577337,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540733690","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73370-6_13","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T20:03:26Z","timestamp":1188417806000},"page":"187-203","source":"Crossref","is-referenced-by-count":35,"title":["Scalable Multi-core LTL Model-Checking"],"prefix":"10.1007","author":[{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1109\/ASE.2003.1240299","volume-title":"Proc. 18th IEEE International Conference on Automated Software Engineering","author":"J. Barnat","year":"2003","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: Parallel Breadth-First Search LTL Model-Checking. In: Proc. 18th IEEE International Conference on Automated Software Engineering, pp. 106\u2013115. IEEE Computer Society, Los Alamitos (2003)"},{"key":"13_CR2","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I.: Property Driven Distribution of Nested DFS. In: Proceedinfs of the 3rd International Workshop on Verification and Computational Logic (VCL 2002 \u2013 held at the PLI 2002 Symposium), University of Southampton, UK, Technical Report DSSE-TR-2002-5 in DSSE, pp. 1\u201310 (2002)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11817963_26","volume-title":"Computer Aided Verification","author":"J. Barnat","year":"2006","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., Moravec, P., Ro\u010dkai, P., \u0160ime\u010dek, P.: DiVinE \u2013 A Tool for Distributed Verification (Tool Paper). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 278\u2013281. Springer, Heidelberg (2006)"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"352","DOI":"10.1007\/978-3-540-30494-4_25","volume-title":"Formal Methods in Computer-Aided Design","author":"L. Brim","year":"2004","unstructured":"Brim, L., \u010cern\u00e1, I., Moravec, P., \u0160im\u0161a, J.: Accepting Predecessors are Better than Back Edges in Distributed LTL Model-Checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 352\u2013366. Springer, Heidelberg (2004)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-45294-X_9","volume-title":"FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science","author":"L. Brim","year":"2001","unstructured":"Brim, L., \u010cern\u00e1, I., Kr\u010d\u00e1l, P., Pel\u00e1nek, R.: Distributed LTL model checking based on negative cycle detection. In: Hariharan, R., Mukund, M., Vinay, V. (eds.) FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a02245, pp. 96\u2013107. Springer, Heidelberg (2001)"},{"key":"13_CR6","unstructured":"Brim, L., \u010cern\u00e1, I., Moravec, P., \u0160im\u0161a, J.: How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors. In: Proceedings of the 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC 2005), pp. 1\u201312 (2005)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/3-540-44829-2_4","volume-title":"Model Checking Software","author":"I. \u010cern\u00e1","year":"2003","unstructured":"\u010cern\u00e1, I., Pel\u00e1nek, R.: Distributed explicit fair cycle detection (set based approach). In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol.\u00a02648, pp. 49\u201373. Springer, Heidelberg (2003)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a02747, pp. 318\u2013327. Springer, Heidelberg (2003)"},{"key":"13_CR9","doi-asserted-by":"publisher","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 in System Design\u00a01, 275\u2013288 (1992)","journal-title":"Formal Methods in System Design"},{"key":"13_CR10","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/298595.298598","volume-title":"Proc. 2nd Workshop on Formal Methods in Software Practice (FMSP-1998)","author":"M. Dwyer","year":"1998","unstructured":"Dwyer, M., Avrunin, G., Corbett, J.: Property specification patterns for finite-state verification. In: Ardis, M. (ed.) Proc. 2nd Workshop on Formal Methods in Software Practice (FMSP-1998), pp. 7\u201315. ACM Press, New York (1998)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-45319-9_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Fisler","year":"2001","unstructured":"Fisler, K., Fraer, R., Kamhi, G., Vardi, M.Y., Yang, Z.: Is there a best symbolic cycle-detection algorithm? In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 420\u2013434. Springer, Heidelberg (2001)"},{"key":"13_CR12","unstructured":"Holzmann, G.: The Design of a Distributed Model Checking Algorithm for SPIN. In: FMCAD, Invited Talk (2006)"},{"key":"13_CR13","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, London (2003)"},{"key":"13_CR14","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. Proc. of the 2nd SPIN Workshop (1996)"},{"issue":"2","key":"13_CR15","doi-asserted-by":"publisher","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 in System Design\u00a029(2), 135\u2013155 (2006)","journal-title":"Formal Methods in System Design"},{"key":"13_CR16","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":"13_CR17","doi-asserted-by":"publisher","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 Transactions on Parallel and Distributed Systems\u00a08(5), 538\u2013543 (1997)","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"13_CR18","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1145\/93385.93442","volume-title":"Proc. ACM Symposium on Principles of Distributed Computing","author":"Z. Manna","year":"1990","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Proc. ACM Symposium on Principles of Distributed Computing, pp. 377\u2013410. ACM Press, New York (1990)"},{"issue":"6","key":"13_CR19","doi-asserted-by":"publisher","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.\u00a039(6), 35\u201346 (2004)","journal-title":"SIGPLAN Not."},{"key":"13_CR20","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, pp. 267\u2013275 (1996)","DOI":"10.1145\/248052.248106"},{"key":"13_CR21","unstructured":"Pel\u00e1nek, R.: BEEM: BEnchmarks for Explicit Model checkers (February 2007), http:\/\/anna.fi.muni.cz\/models\/index.html"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Tarjan, R.: Depth First Search and Linear Graph Algorithms. SIAM Journal on Computing, 146\u2013160 (1972)","DOI":"10.1137\/0201010"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73370-6_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:08:44Z","timestamp":1619503724000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73370-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733690"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73370-6_13","relation":{},"subject":[]}}