{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,6,17]],"date-time":"2023-06-17T23:27:12Z","timestamp":1687044432392},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,2,3]],"date-time":"2010-02-03T00:00:00Z","timestamp":1265155200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2010,5]]},"DOI":"10.1007\/s10009-010-0137-y","type":"journal-article","created":{"date-parts":[[2010,2,2]],"date-time":"2010-02-02T16:13:44Z","timestamp":1265127224000},"page":"155-170","source":"Crossref","is-referenced-by-count":31,"title":["Solving the ignoring problem for partial order reduction"],"prefix":"10.1007","volume":"12","author":[{"given":"Sami","family":"Evangelista","sequence":"first","affiliation":[]},{"given":"Christophe","family":"Pajault","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,2,3]]},"reference":[{"key":"137_CR1","doi-asserted-by":"crossref","unstructured":"Bao, T., Jones, M.: Time-efficient model checking with magnetic disk. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 3440, pp. 526\u2013540. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_34"},{"key":"137_CR2","doi-asserted-by":"crossref","unstructured":"Basten, T., Bosnacki, D.: Enhancing partial-order reduction via process clustering. In: Automated Software Engineering, pp. 245\u2013253. IEEE Computer Society, USA (2001)","DOI":"10.1109\/ASE.2001.989810"},{"key":"137_CR3","doi-asserted-by":"crossref","unstructured":"Bosnacki, D., Holzmann G.J.: Improving spin\u2019s partial-order reduction for breadth-first search. In: SPIN, Model Checking of Software. LNCS, vol. 3639, pp. 91\u2013105. Springer, Berlin (2005)","DOI":"10.1007\/11537328_10"},{"key":"137_CR4","doi-asserted-by":"crossref","unstructured":"Bosnacki D., Leue, S., Lluch-Lafuente, A.: Partial-order reduction for general state exploring algorithms. In: SPIN, Model Checking of Software. LNCS, vol. 3925, pp. 271\u2013287. Springer, Berlin (2006)","DOI":"10.1007\/11691617_16"},{"issue":"3","key":"137_CR5","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/j.entcs.2004.10.019","volume":"128","author":"L. Brim","year":"2005","unstructured":"Brim L., Cern\u00e1 I., Moravec P., Simsa J.: Distributed partial order reduction of state spaces. Electr. Notes Theor. Comput. Sci. 128(3), 63\u201374 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"137_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Computer Aided Verification. LNCS, vol. 1427, pp. 147\u2013158. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028741"},{"key":"137_CR7","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke E.M., Grumberg O., Peled D.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"137_CR8","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. In: Computer Aided Verification. LNCS, vol. 531, pp. 233\u2013242. Springer, Berlin (1990)","DOI":"10.1007\/BFb0023737"},{"key":"137_CR9","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Stern, U.: Using magnetic disk instead of main memory in the Mur\u03d5 Verifier. In: Computer Aided Verification. LNCS, vol. 1427, pp. 172\u2013183. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028743"},{"issue":"2\u20133","key":"137_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. Softw. Tools Technol. Transf. 5(2\u20133), 247\u2013267 (2004)","journal-title":"Softw. Tools Technol. Transf."},{"key":"137_CR11","doi-asserted-by":"crossref","unstructured":"Evangelista, S.: High level petri nets analysis with Helena. In: Applications and Theory of Petri Nets. LNCS, vol. 3536, pp. 455\u2013464. Springer, Berlin (2005)","DOI":"10.1007\/11494744_26"},{"key":"137_CR12","doi-asserted-by":"crossref","unstructured":"Evangelista, S., Kaiser, C., Pradat-Peyre, J.-F., Rousseau, P.: Quasar: a new tool for analysing concurrent programs. In: Reliable Software Technologies. LNCS, vol. 2655, pp. 168\u2013181. Springer, Berlin (2003)","DOI":"10.1007\/3-540-44947-7_12"},{"key":"137_CR13","doi-asserted-by":"crossref","unstructured":"Evangelista, S., Pradat-Peyre, J.-F.: Memory efficient state space storage in explicit software model checking. In: SPIN, Model Checking of Software. LNCS, vol. 3639, pp. 43\u201357. Springer, Berlin (2005)","DOI":"10.1007\/11537328_7"},{"key":"137_CR14","doi-asserted-by":"crossref","unstructured":"Flanagan C., Godefroid P.: Dynamic partial-order reduction for model checking software. In: Principles of Programming Languages, pp. 110\u2013121. ACM, New York (2005)","DOI":"10.1145\/1047659.1040315"},{"key":"137_CR15","doi-asserted-by":"crossref","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.M.: Parallel state space construction for model-checking. In SPIN, Model Checking of Software. LNCS, vol. 2057, pp. 217\u2013234. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45139-0_14"},{"key":"137_CR16","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-order methods for the verification of concurrent systems\u2014an approach to the state-explosion problem. LNCS, vol. 1032. Springer, Berlin (1996)","DOI":"10.1007\/3-540-60761-7"},{"key":"137_CR17","unstructured":"Holzmann, G.J.: State compression in spin: recursive indexing and compression training runs. In: SPIN, Model Checking of Software (1997)"},{"issue":"5","key":"137_CR18","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1\/2","key":"137_CR19","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/BF00625968","volume":"9","author":"C. Norris Ip","year":"1996","unstructured":"Norris Ip C., Dill D.L.: Better verification through symmetry. Formal Methods Syst. Des. 9(1\/2), 41\u201375 (1996)","journal-title":"Formal Methods Syst. Des."},{"key":"137_CR20","unstructured":"Kaiser, C., Pradat-Peyre, J.-F.:Chameneos, a concurrency game for Java, Ada and others. In: Computer Systems and Applications, p. 8 (2003)"},{"key":"137_CR21","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P., Levin, V., Minea, M., Peled, D., Yenigun, H.: Static partial order reduction. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 1384, pp. 345\u2013357. Springer, Berlin (1998)","DOI":"10.1007\/BFb0054182"},{"key":"137_CR22","doi-asserted-by":"crossref","unstructured":"Lerda F., Sisto R. Distributed-memory model checking with SPIN. In: SPIN, Model Checking of Software. LNCS, vol. 1680, pp. 22\u201339. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48234-2_3"},{"key":"137_CR23","unstructured":"Moravec P., Simsa J.: Relaxed cycle condition improves partial order reduction. In: Mathematical and Engineering Methods in Computer Science, pp. 152\u2013159 (2006)"},{"issue":"3","key":"137_CR24","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1023\/A:1014728912264","volume":"20","author":"R. Nalumasu","year":"2000","unstructured":"Nalumasu R., Gopalakrishnan G.: An efficient partial order reduction algorithm with an alternative proviso implementation. Formal Methods Syst. Des. 20(3), 231\u2013247 (2000)","journal-title":"Formal Methods Syst. Des."},{"key":"137_CR25","doi-asserted-by":"crossref","unstructured":"Pel\u00e1nek, R.: BEEM: Benchmarks for explicit model checkers. In: SPIN, Model Checking of Software. LNCS, vol. 4595, pp. 263\u2013267. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73370-6_17"},{"key":"137_CR26","doi-asserted-by":"crossref","unstructured":"Peled, D.: All from one, one for all: on model checking using representatives. In: Computer Aided Verification. LNCS, vol. 697, pp. 409\u2013423. Springer, Berlin (1993)","DOI":"10.1007\/3-540-56922-7_34"},{"key":"137_CR27","doi-asserted-by":"crossref","unstructured":"Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Computer Aided Verification. LNCS, vol. 818, pp. 377\u2013390. Springer, Berlin (1994)","DOI":"10.1007\/3-540-58179-0_69"},{"key":"137_CR28","doi-asserted-by":"crossref","unstructured":"Stern U., Dill, D.L. (1997) Parallelizing the Murphi verifier. In Computer Aided Verification. LNCS, vol. 1254, pp. 256\u2013278. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63166-6_26"},{"issue":"2","key":"137_CR29","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"137_CR30","doi-asserted-by":"crossref","unstructured":"Valmari, A.: Stubborn sets for reduced state space generation. In: Applications and Theory of Petri Nets. LNCS, vol. 483, pp. 491\u2013515. Springer, Berlin (1989)","DOI":"10.1007\/3-540-53863-1_36"},{"issue":"4","key":"137_CR31","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A. Valmari","year":"1992","unstructured":"Valmari A.: A stubborn attack on state explosion. Formal Methods Syst. Des. 1(4), 297\u2013322 (1992)","journal-title":"Formal Methods Syst. Des."},{"key":"137_CR32","doi-asserted-by":"crossref","unstructured":"Valmari, A.: The state explosion problem. In: Lectures on Petri Nets I: Basic Models. LNCS, vol. 1491, pp. 429\u2013528. Springer, Berlin (1998)","DOI":"10.1007\/3-540-65306-6_21"},{"key":"137_CR33","unstructured":"Varpaaniemi, K.: Efficient detection of deadlock in petri nets. Master\u2019s thesis, Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory (1993)"},{"key":"137_CR34","doi-asserted-by":"crossref","unstructured":"Varpaaniemi, K.: On stubborn sets in the verification of linear time temporal properties. In: Applications and Theory of Petri Nets. LNCS, vol. 1420, pp. 124\u2013143. Springer, Berlin (1998)","DOI":"10.1007\/3-540-69108-1_8"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0137-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0137-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0137-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:26Z","timestamp":1559114726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0137-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2,3]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["137"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0137-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2,3]]}}}