{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T12:58:00Z","timestamp":1725541080231},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642103728"},{"type":"electronic","value":"9783642103735"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10373-5_21","type":"book-chapter","created":{"date-parts":[[2009,11,16]],"date-time":"2009-11-16T06:45:27Z","timestamp":1258353927000},"page":"407-425","source":"Crossref","is-referenced-by-count":19,"title":["A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties"],"prefix":"10.1007","author":[{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Ro\u010dkai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-540-73368-3_32","volume-title":"Computer Aided Verification","author":"J. Barnat","year":"2007","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I.: I\/O Efficient Accepting Cycle Detection. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 281\u2013293. Springer, Heidelberg (2007)"},{"key":"21_CR2","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":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a05311, pp. 234\u2013239. Springer, Heidelberg (2008)"},{"key":"21_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":"21_CR5","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. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 49\u201373. Springer, Heidelberg (2003)"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BFb0023737","volume-title":"Computer-Aided Verification","author":"C. Courcoubetics","year":"1991","unstructured":"Courcoubetics, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. In: Clarke, E., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol.\u00a0531, pp. 233\u2013242. Springer, Heidelberg (1991)"},{"key":"21_CR7","unstructured":"DiVinE \u2013 Distributed Verification Environment, Masaryk University Brno, \n                    \n                      http:\/\/divine.fi.muni.cz"},{"key":"21_CR8","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1145\/298595.298598","volume-title":"Proc. Workshop on Formal Methods in Software Practice","author":"M.B. Dwyer","year":"1998","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property Specification Patterns for Finite-State Verification. In: Proc. Workshop on Formal Methods in Software Practice, pp. 7\u201315. ACM Press, New York (1998)"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11691617_1","volume-title":"Model Checking Software","author":"S. Edelkamp","year":"2006","unstructured":"Edelkamp, S., Jabbar, S.: Large-scale directed model checking LTL. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 1\u201318. Springer, Heidelberg (2006)"},{"issue":"2-3","key":"21_CR10","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/s10009-002-0104-3","volume":"5","author":"S. Edelkamp","year":"2004","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. STTT\u00a05(2-3), 247\u2013267 (2004)","journal-title":"STTT"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45139-0_5","volume-title":"Model Checking Software","author":"S. Edelkamp","year":"2001","unstructured":"Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed Explicit Model Checking with HSF-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 57\u201379. Springer, Heidelberg (2001)"},{"issue":"1","key":"21_CR12","doi-asserted-by":"publisher","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.\u00a0345(1), 60\u201382 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/978-3-540-31980-1_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Hammer","year":"2005","unstructured":"Hammer, M., Knapp, A., Merz, S.: Truly On-the-Fly LTL Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 191\u2013205. Springer, Heidelberg (2005)"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1007\/978-3-642-02658-4_32","volume-title":"CAV 2009","author":"R. Kaivola","year":"2009","unstructured":"Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodov\u00e1, A., Taylor, C., Frolov, V., Reeber, E., Naik, A.: Replacing Testing with Formal Verification in Intel Core i7 Processor Execution Engine Validation. In: CAV 2009. LNCS, vol.\u00a05643, pp. 414\u2013429. Springer, Heidelberg (2009)"},{"key":"21_CR15","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.\u00a04595, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.\u00a03440, pp. 174\u2013190. Springer, Heidelberg (2005)"},{"key":"21_CR17","doi-asserted-by":"crossref","unstructured":"Tarjan, R.: Depth First Search and Linear Graph Algorithms. SIAM Journal on Computing, 146\u2013160 (January 1972)","DOI":"10.1137\/0201010"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-540-69738-1_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M.Y. Vardi","year":"2007","unstructured":"Vardi, M.Y.: Automata-Theoretic Model Checking Revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 137\u2013150. Springer, Heidelberg (2007)"},{"key":"21_CR19","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. IEEE Symposium on Logic in Computer Science, pp. 322\u2013331. Computer Society Press (1986)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10373-5_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T07:28:52Z","timestamp":1619767732000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10373-5_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642103728","9783642103735"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10373-5_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}