{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T19:58:59Z","timestamp":1742932739091,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540884781"},{"type":"electronic","value":"9783540884798"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-88479-8_43","type":"book-chapter","created":{"date-parts":[[2008,11,4]],"date-time":"2008-11-04T09:18:43Z","timestamp":1225790323000},"page":"604-618","source":"Crossref","is-referenced-by-count":0,"title":["Squeeze All the Power Out of Your Hardware to Verify Your Software!"],"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"}]}],"member":"297","reference":[{"key":"43_CR1","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I.: Property Driven Distribution of Nested DFS. In: Proceedings 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":"43_CR2","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":"43_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":"43_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-73370-6_13","volume-title":"Model Checking Software","author":"J. Barnat","year":"2007","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: Scalable Multi-core LTL Model-Checkin. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 187\u2013203. Springer, Heidelberg (2007)"},{"key":"43_CR5","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., \u0160ime\u010dek, P.: I\/O Efficient Accepting Cycle Detection. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 281\u2013293. Springer, Heidelberg (2007)"},{"key":"43_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-78800-3_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Brim, L., \u0160ime\u010dek, P., Weber, M.: Revisiting Resistance Speeds Up I\/O-Efficient LTL Model Checking. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 48\u201362. Springer, Heidelberg (2008)"},{"issue":"1","key":"43_CR7","first-page":"79","volume":"198","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Ro\u010dkai, P.: Shared Hash Tables in Parallel Model Checking. ENTCS\u00a0198(1), 79\u201391 (2008)","journal-title":"ENTCS"},{"key":"43_CR8","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 \u2014 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":"43_CR9","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"},{"key":"43_CR10","doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness Checking as Safety Checking. Electr. Notes Theor. Comput. Sci.\u00a066(2) (2002)","DOI":"10.1016\/S1571-0661(04)80410-9"},{"issue":"1","key":"43_CR11","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":"43_CR12","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.) TACAS 2001. LNCS, vol.\u00a02031, pp. 543\u2013558. Springer, Heidelberg (2001)"},{"key":"43_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"issue":"2","key":"43_CR14","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2005.10.015","volume":"135","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. Electronic Notes in Theoretical Computer Science\u00a0135(2), 3\u201318 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"43_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.) SPIN 2003. LNCS, vol.\u00a02648, pp. 49\u201373. Springer, Heidelberg (2003)"},{"key":"43_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"43_CR17","volume-title":"Model Checking","author":"E.M. Clarke Jr.","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"43_CR18","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":"43_CR19","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":"43_CR20","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)"},{"key":"43_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"J. Esparza","year":"2005","unstructured":"Esparza, J., Schwoon, S.: 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":"43_CR22","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.) TACAS 2001. LNCS, vol.\u00a02031, pp. 420\u2013434. Springer, Heidelberg (2001)"},{"key":"43_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/978-3-540-24730-2_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Geldenhuys","year":"2004","unstructured":"Geldenhuys, J., Valmari, A.: Tarjan\u2019s algorithm makes on-the-fly LTL verification more efficient. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 205\u2013219. Springer, Heidelberg (2004)"},{"key":"43_CR24","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.: Achieving speedups in distributed symbolic reachability analysis through asynchronous computation. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 129\u2013145. Springer, Heidelberg (2005)"},{"key":"43_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"43_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","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.: To Store Or Not To Store Reloaded. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 51\u201366. Springer, Heidelberg (2007)"},{"key":"43_CR27","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)"},{"issue":"10","key":"43_CR28","doi-asserted-by":"publisher","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 Transactions on Software Engineering\u00a033(10), 659\u2013674 (2007)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"43_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/978-3-540-30579-8_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Jabbar","year":"2005","unstructured":"Jabbar, S., Edelkamp, S.: I\/O Efficient Directed Model Checking. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 313\u2013329. Springer, Heidelberg (2005)"},{"key":"43_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-540-24732-6_10","volume-title":"Model Checking Software","author":"M. Jones","year":"2004","unstructured":"Jones, M., Mercer, E.: Explicit State Model Checking with Hopper. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 146\u2013150. Springer, Heidelberg (2004)"},{"key":"43_CR31","unstructured":"Korf, R.: Best-First Frontier Search with Delayed Duplicate Detection. In: AAAI 2004, pp. 650\u2013657. AAAI Press \/ The MIT Press (2004)"},{"key":"43_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-39893-6_19","volume-title":"Formal Methods and Software Engineering","author":"L. Kristensen","year":"2003","unstructured":"Kristensen, L., Mailund, T.: Efficient Path Finding with the Sweep-Line Method Using External Storage. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol.\u00a02885, pp. 319\u2013337. Springer, Heidelberg (2003)"},{"key":"43_CR33","unstructured":"Lafuente, A.L.: Simplified distributed LTL model checking by localizing cycles. Technical Report 00176, Institut f\u00fcr Informatik, University Freiburg, Germany (July 2002)"},{"key":"43_CR34","unstructured":"Munagala, K., Ranade, A.: I\/O-Complexity of Graph Algorithms. In: SODA 1999, Philadelphia, PA, USA, pp. 687\u2013694. Society for Industrial and Applied Mathematics (1999)"},{"key":"43_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.) SPIN 2004. LNCS, vol.\u00a02989, pp. 5\u201322. Springer, Heidelberg (2004)"},{"key":"43_CR36","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)"},{"issue":"2\u20133","key":"43_CR37","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-003-0121-x","volume":"5","author":"V. Schuppan","year":"2004","unstructured":"Schuppan, V., Biere, A.: Efficient Reduction of Finite State Model Checking to Reachability Analysis. International Journal on Software Tools for Technology Transfer (STTT)\u00a05(2\u20133), 185\u2013204 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"43_CR38","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 Disk Instead of Main Memory in the Murphi Verifier. In: Vardi, M., Y. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 172\u2013183. Springer, Heidelberg (1998)"},{"key":"43_CR39","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":"43_CR40","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. Vardi","year":"2007","unstructured":"Vardi, M.: Automata-Theoretic Model Checking Revisited. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 137\u2013150. Springer, Heidelberg (2007)"},{"key":"43_CR41","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":["Communications in Computer and Information Science","Leveraging Applications of Formal Methods, Verification and Validation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-88479-8_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T22:30:53Z","timestamp":1557873053000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-88479-8_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540884781","9783540884798"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-88479-8_43","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2008]]}}}