{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T18:38:30Z","timestamp":1771699110889,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":74,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642032394","type":"print"},{"value":"9783642032400","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03240-0_7","type":"book-chapter","created":{"date-parts":[[2009,7,27]],"date-time":"2009-07-27T14:27:38Z","timestamp":1248704858000},"page":"37-52","source":"Crossref","is-referenced-by-count":34,"title":["Fighting State Space Explosion: Review and Evaluation"],"prefix":"10.1007","author":[{"given":"Radek","family":"Pel\u00e1nek","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I.: Property driven distribution of nested DFS. In: Proc. of Workshop on Verification and Computational Logic, number DSSE-TR-2002-5 in DSSE Technical Report, pp. 1\u201310. University of Southampton, UK (2002)"},{"key":"7_CR2","first-page":"106","volume-title":"Proc. of Automated Software Engineering (ASE 2003)","author":"J. Barnat","year":"2003","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: Parallel breadth-first search LTL model-checking. In: Proc. of Automated Software Engineering (ASE 2003), pp. 106\u2013115. IEEE Computer Society, Los Alamitos (2003)"},{"issue":"1","key":"7_CR3","first-page":"21","volume":"133","author":"J. Barnat","year":"2005","unstructured":"Barnat, J., Brim, L., Chaloupka, J.: From distributed memory cycle detection to parallel LTL model checking. ENTCS\u00a0133(1), 21\u201339 (2005)","journal-title":"ENTCS"},{"key":"7_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., Rockai, P.: Scalable multi-core LTL model-checking. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 187\u2013203. Springer, Heidelberg (2007)"},{"key":"7_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-45139-0_13","volume-title":"Model Checking Software","author":"J. Barnat","year":"2001","unstructured":"Barnat, J., Brim, L., St\u0159\u00edbrn\u00e1, J.: Distributed LTL model-checking in SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 200\u2013216. Springer, Heidelberg (2001)"},{"key":"7_CR6","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., Rockai, P., \u0160ime\u010dek, P.: DiVinE - a tool for distributed verification. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 278\u2013281. Springer, Heidelberg (2006), http:\/\/anna.fi.muni.cz\/divine"},{"key":"7_CR7","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 i\/o efficient accepting cycle detection. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 281\u2013293. Springer, Heidelberg (2007)"},{"key":"7_CR8","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)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-540-45069-6_40","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"2003","unstructured":"Behrmann, G., Larsen, K.G., Pel\u00e1nek, R.: To store or not to store. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 433\u2013445. Springer, Heidelberg (2003)"},{"key":"7_CR10","volume-title":"Principles of the SPIN Model Checker","author":"M. Ben-Ari","year":"2008","unstructured":"Ben-Ari, M.: Principles of the SPIN Model Checker. Springer, Heidelberg (2008)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1007\/3-540-45657-0_50","volume-title":"Computer Aided Verification","author":"S. Blom","year":"2002","unstructured":"Blom, S., van de Pol, J.: State space reduction by proving confluence. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 596\u2013609. Springer, Heidelberg (2002)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-44829-2_6","volume-title":"Model Checking Software","author":"D. Bosnacki","year":"2003","unstructured":"Bosnacki, D.: A light-weight algorithm for model checking with symmetry reduction and weak fairness. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 89\u2013103. Springer, Heidelberg (2003)"},{"key":"7_CR13","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.) FSTTCS 2001. LNCS, vol.\u00a02245, pp. 96\u2013107. Springer, Heidelberg (2001)"},{"key":"7_CR14","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. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 49\u201373. Springer, Heidelberg (2003)"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/3-540-45319-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Christensen","year":"2001","unstructured":"Christensen, S., Kristensen, L.M., Mailund, T.: A sweep-line method for state space exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 450\u2013464. Springer, Heidelberg (2001)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-540-30494-4_26","volume-title":"Formal Methods in Computer-Aided Design","author":"P.C. Dillinger","year":"2004","unstructured":"Dillinger, P.C., Manolios, P.: Bloom filters in probabilistic verification. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 367\u2013381. Springer, Heidelberg (2004)"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-540-24732-6_5","volume-title":"Model Checking Software","author":"P.C. Dillinger","year":"2004","unstructured":"Dillinger, P.C., Manolios, P.: Fast and accurate bitstate verification for SPIN. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 57\u201375. Springer, Heidelberg (2004)"},{"key":"7_CR18","first-page":"241","volume-title":"Proc. of Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX)","author":"Y. Dong","year":"1999","unstructured":"Dong, Y., Ramakrishnan, C.R.: An optimizing compiler for efficient model checking. In: Proc. of Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XII) and Protocol Specification, Testing and Verification (PSTV XIX), pp. 241\u2013256. Kluwer, Dordrecht (1999)"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/11691372_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.B. Dwyer","year":"2006","unstructured":"Dwyer, M.B., Hatcliff, J., Hoosier, M., Ranganath, V.P.: Evaluating the effectiveness of slicing for model reduction of concurrent object-oriented programs. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 73\u201389. Springer, Heidelberg (2006)"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-31980-1_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.A. Emerson","year":"2005","unstructured":"Emerson, E.A., Wahl, T.: Dynamic symmetry reduction. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 382\u2013396. Springer, Heidelberg (2005)"},{"issue":"2-3","key":"7_CR21","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1016\/S0167-6423(02)00133-8","volume":"47","author":"J.C. Fernandez","year":"2003","unstructured":"Fernandez, J.C., Bozga, M., Ghirvu, L.: State space reduction based on live variables analysis. Journal of Science of Computer Programming (SCP)\u00a047(2-3), 203\u2013220 (2003)","journal-title":"Journal of Science of Computer Programming (SCP)"},{"key":"7_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","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.) SPIN 2001. LNCS, vol.\u00a02057, pp. 217\u2013234. Springer, Heidelberg (2001)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-540-24732-6_3","volume-title":"Model Checking Software","author":"J. Geldenhuys","year":"2004","unstructured":"Geldenhuys, J.: State caching reconsidered. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 23\u201338. Springer, Heidelberg (2004)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/3-540-48234-2_2","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"J. Geldenhuys","year":"1999","unstructured":"Geldenhuys, J., de Villiers, P.J.A.: Runtime efficient state compaction in SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 12\u201321. Springer, Heidelberg (1999)"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/3-540-44829-2_9","volume-title":"Model Checking Software","author":"J. Geldenhuys","year":"2003","unstructured":"Geldenhuys, J., Valmari, A.: A nearly memory-optimal data structure for sets and mappings. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 136\u2013150. Springer, Heidelberg (2003)"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-60761-7","volume-title":"Partial-Order Methods for the Verification of Concurrent Systems","author":"P. Godefroid","year":"1996","unstructured":"Godefroid, P.: Partial-order methods for the verification of concurrent systems: an approach to the state-explosion problem. In: Godefroid, P. (ed.) Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol.\u00a01032, p. 142. Springer, Heidelberg (1996)"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/3-540-56496-9_15","volume-title":"Computer Aided Verification","author":"P. Godefroid","year":"1993","unstructured":"Godefroid, P., Holzmann, G.J., Pirottin, D.: State space caching revisited. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 178\u2013191. Springer, Heidelberg (1993)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/3-540-46002-0_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Godefroid","year":"2002","unstructured":"Godefroid, P., Khurshid, S.: Exploring very large state spaces using genetic algorithms. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 266\u2013280. Springer, Heidelberg (2002)"},{"key":"7_CR30","unstructured":"Gregoire, J.: State space compression in spin with GETSs. In: Proc. Second SPIN Workshop, Rutgers University, New Brunswick, New Jersey (1996)"},{"issue":"4","key":"7_CR31","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/s10009-003-0130-9","volume":"6","author":"A. Groce","year":"2004","unstructured":"Groce, A., Visser, W.: Heuristics for model checking java programs. Software Tools for Technology Transfer (STTT)\u00a06(4), 260\u2013276 (2004)","journal-title":"Software Tools for Technology Transfer (STTT)"},{"issue":"3","key":"7_CR32","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-540-73370-6_8","volume-title":"Model Checking Software","author":"G. Gueta","year":"2007","unstructured":"Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 95\u2013112. Springer, Heidelberg (2007)"},{"key":"7_CR34","unstructured":"Haslum, P.: Model checking by random walk. In: Proc. of ECSEL Workshop (1999)"},{"issue":"4","key":"7_CR35","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1023\/A:1026599015809","volume":"13","author":"J. Hatcliff","year":"2000","unstructured":"Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Higher Order Symbol. Comput.\u00a013(4), 315\u2013353 (2000)","journal-title":"Higher Order Symbol. Comput."},{"issue":"2","key":"7_CR36","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1002\/j.1538-7305.1990.tb00101.x","volume":"69","author":"G.J. Holzmann","year":"1990","unstructured":"Holzmann, G.J.: Algorithms for automated protocol verification. AT&T Technical Journal\u00a069(2), 32\u201344 (1990)","journal-title":"AT&T Technical Journal"},{"key":"7_CR37","first-page":"301","volume-title":"Proc. of Protocol Specification, Testing, and Verification","author":"G.J. Holzmann","year":"1995","unstructured":"Holzmann, G.J.: An analysis of bitstate hashing. In: Proc. of Protocol Specification, Testing, and Verification, pp. 301\u2013314. Chapman & Hall, Boca Raton (1995)"},{"key":"7_CR38","unstructured":"Holzmann, G.J.: State compression in SPIN: Recursive indexing and compression training runs. In: Proc. of SPIN Workshop (1997)"},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Godefroid, P., Pirottin, D.: Coverage preserving reduction strategies for reachability analysis. In: Proc. of Protocol Specification, Testing, and Verification (1992)","DOI":"10.1016\/B978-0-444-89874-6.50028-3"},{"key":"7_CR40","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-0-387-34878-0_13","volume-title":"Proc. of Formal Description Techniques VII","author":"G.J. Holzmann","year":"1995","unstructured":"Holzmann, G.J., Peled, D.: An improvement in formal verification. In: Proc. of Formal Description Techniques VII, pp. 197\u2013211. Chapman & Hall, Ltd., Boca Raton (1995)"},{"issue":"1","key":"7_CR41","first-page":"270","volume":"3","author":"G.J. Holzmann","year":"1998","unstructured":"Holzmann, G.J., Puri, A.: A minimized automaton representation of reachable states. Software Tools for Technology Transfer (STTT)\u00a03(1), 270\u2013278 (1998)","journal-title":"Software Tools for Technology Transfer (STTT)"},{"issue":"10","key":"7_CR42","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":"7_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-46017-9_5","volume-title":"Model Checking Software","author":"R. Iosif","year":"2002","unstructured":"Iosif, R.: Symmetry reduction criteria for software model checking. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol.\u00a02318, pp. 22\u201341. Springer, Heidelberg (2002)"},{"issue":"1\u20132","key":"7_CR44","first-page":"41","volume":"9","author":"C.N. Ip","year":"1996","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design\u00a09(1\u20132), 41\u201375 (1996)","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"7_CR45","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10009-003-0115-8","volume":"7","author":"M.D. Jones","year":"2005","unstructured":"Jones, M.D., Sorber, J.: Parallel search for LTL violations. Software Tools for Technology Transfer (STTT)\u00a07(1), 31\u201342 (2005)","journal-title":"Software Tools for Technology Transfer (STTT)"},{"key":"7_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/BFb0035392","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.P. Krimm","year":"1997","unstructured":"Krimm, J.P., Mounier, L.: Compositional state space generation from Lotos programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol.\u00a01217, pp. 239\u2013258. Springer, Heidelberg (1997)"},{"key":"7_CR47","first-page":"574","volume-title":"Proc. of Computer-Aided Design (CAD 1999)","author":"A. Kuehlmann","year":"1999","unstructured":"Kuehlmann, A., McMillan, K.L., Brayton, R.K.: Probabilistic state space search. In: Proc. of Computer-Aided Design (CAD 1999), pp. 574\u2013579. IEEE Press, Los Alamitos (1999)"},{"key":"7_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"569","DOI":"10.1007\/3-540-45657-0_48","volume-title":"Computer Aided Verification","author":"R.P.. Kurshan","year":"2002","unstructured":"Kurshan, R.P., Levin, V., Yenig\u00fcn, H.: Compressing transitions for model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 569\u2013581. Springer, Heidelberg (2002)"},{"key":"7_CR49","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/REAL.1997.641265","volume-title":"Proc. of Real-Time Systems Symposium (RTSS 1997)","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Efficient verification of real-time systems: Compact data structure and state-space reduction. In: Proc. of Real-Time Systems Symposium (RTSS 1997), pp. 14\u201324. IEEE Computer Society Press, Los Alamitos (1997)"},{"key":"7_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-48234-2_3","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"F. Lerda","year":"1999","unstructured":"Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, p. 22. Springer, Heidelberg (1999)"},{"key":"7_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/3-540-45139-0_6","volume-title":"Model Checking Software","author":"F. Lerda","year":"2001","unstructured":"Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 80\u2013102. Springer, Heidelberg (2001)"},{"issue":"5","key":"7_CR52","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1145\/55483.55496","volume":"17","author":"F. Lin","year":"1987","unstructured":"Lin, F., Chu, P., Liu, M.: Protocol verification using reachability analysis: the state space explosion problem and relief strategies. Computer Communication Review\u00a017(5), 126\u2013134 (1987)","journal-title":"Computer Communication Review"},{"key":"7_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/3-540-58179-0_49","volume-title":"Computer Aided Verification","author":"M. Mihail","year":"1994","unstructured":"Mihail, M., Papadimitriou, C.H.: On the random walk method for protocol testing. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 132\u2013141. Springer, Heidelberg (1994)"},{"key":"7_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-540-24730-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Mailund","year":"2004","unstructured":"Mailund, T., Westergaard, W.: Obtaining memory-efficient reachability graph representations using the sweep-line method. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 177\u2013191. Springer, Heidelberg (2004)"},{"key":"7_CR55","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1016\/S0140-3664(97)00075-3","volume":"20","author":"K. Ozdemir","year":"1997","unstructured":"Ozdemir, K., Ural, H.: Protocol validation by simultaneous reachability analysis. Computer Communications\u00a020, 772\u2013788 (1997)","journal-title":"Computer Communications"},{"key":"7_CR56","unstructured":"Parreaux, B.: Difference compression in SPIN. In: Proc. of Workshop on automata theoric verification with the SPIN model checker (SPIN 1998) (1998)"},{"key":"7_CR57","unstructured":"Pel\u00e1nek, R.: Evaluation of on-the-fly state space reductions. In: Proc. of Mathematical and Engineering Methods in Computer Science (MEMICS 2005), pp. 121\u2013127 (2005)"},{"key":"7_CR58","unstructured":"Pel\u00e1nek, R.: Web portal for benchmarking explicit model checkers. Technical Report FIMU-RS-2006-03, Masaryk University Brno (2006)"},{"key":"7_CR59","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":"7_CR60","first-page":"98","volume-title":"Proc. of Formal Methods for Industrial Critical Systems (FMICS 2005)","author":"R. Pel\u00e1nek","year":"2005","unstructured":"Pel\u00e1nek, R., Han\u017el, T., \u010cern\u00e1, I., Brim, L.: Enhancing random walk state space exploration. In: Proc. of Formal Methods for Industrial Critical Systems (FMICS 2005), pp. 98\u2013105. ACM Press, New York (2005)"},{"key":"7_CR61","doi-asserted-by":"crossref","unstructured":"Pel\u00e1nek, R., Roseck\u00fd, V., Moravec, P.: Complementarity of error detection techniques. In: Proc. of Parallel and Distributed Methods in verifiCation (PDMC) (2008)","DOI":"10.1016\/j.entcs.2008.11.013"},{"key":"7_CR62","unstructured":"Pel\u00e1nek, R., Roseck\u00fd, V., \u0160ed\u011bnka, J.: Evaluation of state caching and state compression techniques. Technical Report FIMU-RS-2008-02, Masaryk University Brno (2008)"},{"key":"7_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1007\/3-540-58179-0_69","volume-title":"Computer Aided Verification","author":"D. Peled","year":"1994","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 377\u2013390. Springer, Heidelberg (1994)"},{"issue":"1-4","key":"7_CR64","doi-asserted-by":"crossref","first-page":"245","DOI":"10.3233\/FI-2000-43123413","volume":"43","author":"W. Penczek","year":"2000","unstructured":"Penczek, W., Szreter, M., Gerth, R., Kuiper, R.: Improving partial order reductions for universal branching time properties. Fundamenta Informaticae\u00a043(1-4), 245\u2013267 (2000)","journal-title":"Fundamenta Informaticae"},{"issue":"4","key":"7_CR65","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/s10009-004-0149-6","volume":"6","author":"G.D. Penna","year":"2004","unstructured":"Penna, G.D., Intrigila, B., Melatti, I., Tronci, E., Zilli, M.V.: Exploiting transition locality in automatic verification of finite state concurrent systems. Software Tools for Technology Transfer (STTT)\u00a06(4), 320\u2013341 (2004)","journal-title":"Software Tools for Technology Transfer (STTT)"},{"key":"7_CR66","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. Logics and models of concurrent systems, 123\u2013144 (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"7_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-540-24730-2_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Qian","year":"2004","unstructured":"Qian, K., Nymeyer, A.: Guided invariant model checking based on abstraction and symbolic pattern databases. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 497\u2013511. Springer, Heidelberg (2004)"},{"key":"7_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-540-24730-2_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Schmidt","year":"2004","unstructured":"Schmidt, K.: Automated generation of a progress measure for the sweep-line method. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 192\u2013204. Springer, Heidelberg (2004)"},{"key":"7_CR69","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-73370-6_9","volume-title":"Model Checking Software","author":"J.P. Self","year":"2007","unstructured":"Self, J.P., Mercer, E.G.: On-the-fly dynamic dead variable analysis. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 113\u2013130. Springer, Heidelberg (2007)"},{"key":"7_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/3-540-44585-4_9","volume-title":"Computer Aided Verification","author":"A.P. Sistla","year":"2001","unstructured":"Sistla, A.P., Godefroid, P.: Symmetry and reduced symmetry in model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 91\u2013103. Springer, Heidelberg (2001)"},{"key":"7_CR71","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: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 172\u2013183. Springer, Heidelberg (1998)"},{"key":"7_CR72","first-page":"332","volume-title":"Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Kozen, D. (ed.) Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pp. 332\u2013344. IEEE Computer Society Press, Los Alamitos (1986)"},{"key":"7_CR73","unstructured":"Visser, W.: Memory efficient state storage in SPIN. In: Proc. of SPIN Workshop, pp. 21\u201335 (1996)"},{"key":"7_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-540-73368-3_43","volume-title":"Computer Aided Verification","author":"T. Wahl","year":"2007","unstructured":"Wahl, T.: Adaptive symmetry reduction. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 393\u2013405. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03240-0_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,21]],"date-time":"2020-05-21T00:43:00Z","timestamp":1590021780000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03240-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642032394","9783642032400"],"references-count":74,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03240-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}