{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:53:27Z","timestamp":1725512007256},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540709510"},{"type":"electronic","value":"9783540709527"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-70952-7_2","type":"book-chapter","created":{"date-parts":[[2007,6,26]],"date-time":"2007-06-26T08:40:01Z","timestamp":1182847201000},"page":"23-34","source":"Crossref","is-referenced-by-count":1,"title":["Distributed Verification: Exploring the Power of Raw Computing Power"],"prefix":"10.1007","author":[{"given":"Lubo\u0161","family":"Brim","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-36383-1_1","volume-title":"Experimental Algorithmics","author":"D. Bader","year":"2002","unstructured":"Bader, D., Moret, B., Sanders, P.: Algorithm Engineering for Parallel Computation. In: Fleischer, R., Moret, B.M.E., Schmidt, E.M. (eds.) Experimental Algorithmics. LNCS, vol.\u00a02547, pp. 1\u201323. Springer, Heidelberg (2002)"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"526","DOI":"10.1007\/978-3-540-31980-1_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Bao","year":"2005","unstructured":"Bao, T., Jones, M.: Time-Efficient Model Checking with Magnetic Disks. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 526\u2013540. Springer, Heidelberg (2005)"},{"key":"2_CR3","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 Press, Los Alamitos (2003)"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Barnat, J., \u010cern\u00e1, I.: Distributed Breadth-First Search LTL Model Checking. Formal Methods in System Design, to appear (2006)","DOI":"10.1007\/s10703-006-0009-y"},{"key":"2_CR5","unstructured":"Barnat, J.: Distributed Memory LTL Model Checking. PhD thesis, Faculty of Informatics, Masaryk University Brno (2004)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/10722167_19","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"2000","unstructured":"Behrmann, G., Hune, T.S., Vaandrager, F.W.: Distributed Timed Model Checking \u2013 How the Search Order Matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 216\u2013231. Springer, Heidelberg (2000)"},{"issue":"1","key":"2_CR7","doi-asserted-by":"publisher","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\u00a07(1), 43\u201360 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"1","key":"2_CR8","doi-asserted-by":"publisher","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\u00a07(1), 74\u201386 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/3-540-45319-9_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Bollig","year":"2001","unstructured":"Bollig, B., Leucker, M., Weber, M.: Parallel Model Checking for the Alternation Free \u03bc-Calculus. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, p. 543. Springer, Heidelberg (2001)"},{"key":"2_CR10","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":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/3-540-45627-9_16","volume-title":"SOFSEM 2001: Theory and Practice of Informatics","author":"L. Brim","year":"2001","unstructured":"Brim, L., \u010cern\u00e1, I., Kr\u010d\u00e1l, P., Pel\u00e1nek, R.: How to Employ Reverse Search in Distributed Single-Source Shortest Paths. In: Pacholski, L., Ru\u017ei\u010dka, P. (eds.) SOFSEM 2001. LNCS, vol.\u00a02234, pp. 191\u2013200. Springer, Heidelberg (2001)"},{"key":"2_CR12","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":"2_CR13","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: 4th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC\u201905), July (2005)"},{"key":"2_CR14","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":"2_CR15","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":"2_CR16","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s101070050058","volume":"85","author":"B.V. Cherkassky","year":"1999","unstructured":"Cherkassky, B.V., Goldberg, A.V.: Negative-Cycle Detection Algorithms. Mathematical Programming\u00a085, 277\u2013311 (1999)","journal-title":"Mathematical Programming"},{"key":"2_CR17","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":"2_CR18","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":"2_CR19","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.) Model Checking Software. LNCS, vol.\u00a03925, pp. 1\u201318. Springer, Heidelberg (2006)"},{"key":"2_CR20","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":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/3-540-45139-0_14","volume-title":"Model Checking Software","author":"H. Garavel","year":"2001","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.: Parallel State Space Construction for Model-Checking. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol.\u00a02057, pp. 216\u2013234. Springer, Heidelberg (2001)"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/11560548_12","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Grumberg","year":"2005","unstructured":"Grumberg, O., Heyman, T., Ifergan, N., Schuster, A.: \u201dachieving speedups in distributed symbolic reachability analysis through asynchronous computation\u201d. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 129\u2013145. Springer, Heidelberg (2005)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/3-540-44585-4_32","volume-title":"Computer Aided Verification","author":"O. Grumberg","year":"2001","unstructured":"Grumberg, O., Heyman, T., Schuster, A.: Distributed Model Checking for \u03bc-calculus. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 350\u2013362. Springer, Heidelberg (2001)"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-70952-7_4","volume-title":"Formal Methods: Applications and Technology","author":"M. Hammer","year":"2007","unstructured":"Hammer, M., Weber, M.: \u201dTo Store or Not To Store\u201d reloaded: Reclaiming memory on demand. In: Brim, L., Haverkort, B., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 52\u201367. Springer, Heidelberg (2007)"},{"key":"2_CR25","first-page":"12","volume-title":"Proc. 8th Int. Workshop on Petri Net and Performance Models","author":"B.R. Haverkort","year":"1999","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: Proc. 8th Int. Workshop on Petri Net and Performance Models, pp. 12\u201321. IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"2_CR26","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)"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Peled, D., Yannakakis, M.: On Nested Depth First Search. In: Proc. SPIN Workshop on Model Checking of Software, pp. 23\u201332. American Mathematical Society (1996)","DOI":"10.1090\/dimacs\/032\/03"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/11609773_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Jabbar","year":"2005","unstructured":"Jabbar, S., Edelkamp, S.: Parallel External Directed Model Checking with Linear I\/O. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 237\u2013251. Springer, Heidelberg (2005)"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-3-540-24732-6_2","volume-title":"Model Checking Software","author":"R. Pel\u00e1nek","year":"2004","unstructured":"Pel\u00e1nek, R.: Typical Structural Properties of State Spaces. In: Graf, S., Mounier, L. (eds.) Model Checking Software. LNCS, vol.\u00a02989, pp. 5\u201322. Springer, Heidelberg (2004)"},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-40922-X_10","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Ravi","year":"2000","unstructured":"Ravi, K., Bloem, R., Somenzi, F.: A Comparative Study of Symbolic Algorithms for the Computation of Fair Cycles. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 143\u2013160. Springer, Heidelberg (2000)"},{"issue":"5","key":"2_CR31","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0020-0190(85)90024-9","volume":"20","author":"J. Reif","year":"1985","unstructured":"Reif, J.: Depth-first Search is Inherently Sequential. Information Proccesing Letters\u00a020(5), 229\u2013234 (1985)","journal-title":"Information Proccesing Letters"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0028743","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1998","unstructured":"Stern, U., Dill, D.L.: Using magnetic disc instead of main memory in the mur\u03d5 verifier. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 172\u2013183. Springer, Heidelberg (1998)"},{"key":"2_CR33","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"},{"key":"2_CR34","first-page":"322","volume-title":"Proc. IEEE Symposium on Logic in Computer Science","author":"M.Y. Vardi","year":"1986","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. IEEE Computer Society Press, Los Alamitos (1986)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Applications and Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70952-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T16:34:51Z","timestamp":1556555691000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70952-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540709510","9783540709527"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70952-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}