{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,8,25]],"date-time":"2022-08-25T17:51:44Z","timestamp":1661449904543},"reference-count":65,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,1,30]],"date-time":"2018-01-30T00:00:00Z","timestamp":1517270400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2019,8]]},"DOI":"10.1007\/s10009-018-0484-7","type":"journal-article","created":{"date-parts":[[2018,1,30]],"date-time":"2018-01-30T06:55:14Z","timestamp":1517295314000},"page":"365-400","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Fast detection of concurrency errors by state space traversal with randomization and early backtracking"],"prefix":"10.1007","volume":"21","author":[{"given":"Pavel","family":"Par\u00edzek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ond\u0159ej","family":"Lhot\u00e1k","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,1,30]]},"reference":[{"key":"484_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Proceedings of POPL. ACM (2014)","DOI":"10.1145\/2535838.2535845"},{"issue":"12","key":"484_CR2","doi-asserted-by":"publisher","first-page":"1272","DOI":"10.1016\/j.scico.2011.03.001","volume":"77","author":"J Barnat","year":"2012","unstructured":"Barnat, J., Brim, L., Rockai, P.: On-the-fly parallel model checking algorithm that is optimal for verification of weak LTL properties. Sci. Comput. Program. 77(12), 1272\u20131288 (2012)","journal-title":"Sci. Comput. Program."},{"key":"484_CR3","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Hune, T., Vaandrager, F.: Distributing timed model checking\u2014how the search order matters. In: Proceedings of CAV, LNCS, vol. 1855 (2000)","DOI":"10.1007\/10722167_19"},{"key":"484_CR4","doi-asserted-by":"crossref","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. J. Satisf. Boolean Model. Comput. (JSAT) 4, 75\u201397 (2008)","journal-title":"J. Satisf. Boolean Model. Comput. (JSAT)"},{"key":"484_CR5","volume-title":"Beam Search. Encyclopedia of Artificial Intelligence","author":"R Bisiani","year":"1992","unstructured":"Bisiani, R.: Beam Search. Encyclopedia of Artificial Intelligence. Wiley, New York (1992)"},{"key":"484_CR6","doi-asserted-by":"crossref","unstructured":"Burckhardt, S., Kothari, P., Musuvathi, M., Nagarakatte, S.: A Randomized scheduler with probabilistic guarantees of finding bugs. In: Proceedings of ASPLOS. ACM (2010)","DOI":"10.1145\/1736020.1736040"},{"issue":"1","key":"484_CR7","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1287\/ijoc.10.1.82","volume":"10","author":"G Ciardo","year":"1998","unstructured":"Ciardo, G., Gluckman, J., Nicol, D.: Distributed state space generation of discrete-state stochastic models. INFORMS J. Comput. 10(1), 82\u201393 (1998)","journal-title":"INFORMS J. Comput."},{"key":"484_CR8","doi-asserted-by":"crossref","unstructured":"Coons, K.E., Burckhardt, S., Musuvathi, M.: GAMBIT: effective unit testing for concurrency libraries. In: Proceedings of PPoPP. ACM (2010)","DOI":"10.1145\/1693453.1693458"},{"key":"484_CR9","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Elbaum, S.G., Person, S., Purandare, R.: Parallel randomized state-space search. In: Proceedings of ICSE, IEEE CS (2007)","DOI":"10.21236\/ADA459092"},{"issue":"2\u20133","key":"484_CR10","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/B:FORM.0000040028.49845.67","volume":"25","author":"M Dwyer","year":"2004","unstructured":"Dwyer, M., Hatcliff, J., Robby, Ranganath, V.: Exploiting object escape and locking information in artial-order reductions for concurrent object-oriented programs. Formal Methods Syst. Des. 25(2\u20133), 199\u2013240 (2004)","journal-title":"Formal Methods Syst. Des."},{"key":"484_CR11","doi-asserted-by":"crossref","unstructured":"Dwyer, M.B., Person, S., Elbaum, S.G.: Controlling factors in evaluating path-sensitive error detection techniques. In: Proceedings of SIGSOFT FSE. ACM (2006)","DOI":"10.21236\/ADA459081"},{"issue":"2\u20133","key":"484_CR12","doi-asserted-by":"publisher","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. Int. J. Softw. Tools Technol. Transf. 5(2\u20133), 247\u2013267 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"484_CR13","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Schuppan, V., Bosnacki, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Proceedings of 5th International Workshop on Model Checking and Artificial Intelligence, LNCS, vol. 5348 (2008)","DOI":"10.1007\/978-3-642-00431-5_5"},{"key":"484_CR14","doi-asserted-by":"crossref","unstructured":"Een, N., Sorensson, N.: An extensible SAT-solver. In: Proceedings of SAT, LNCS, vol. 2919 (2003)","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"484_CR15","doi-asserted-by":"crossref","unstructured":"Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. In: Proceedings of POPL. ACM (2011)","DOI":"10.1145\/1926385.1926432"},{"issue":"4","key":"484_CR16","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1016\/j.jlap.2008.11.003","volume":"78","author":"TAN Engels","year":"2009","unstructured":"Engels, T.A.N., Groote, J.F., van Weerdenburg, M.J., Willemse, T.A.C.: Search algorithms for automated validation. J. Logic Algebr. Program. 78(4), 274\u2013287 (2009)","journal-title":"J. Logic Algebr. Program."},{"key":"484_CR17","doi-asserted-by":"crossref","unstructured":"Farzan, A., Holzer, A., Razavi, N., Veith, H.: Con2colic testing. In: Proceedings of ESEC\/FSE. ACM (2013)","DOI":"10.1145\/2491411.2491453"},{"key":"484_CR18","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of POPL. ACM (2005)","DOI":"10.1145\/1040305.1040315"},{"key":"484_CR19","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Partial-order methods for the verification of concurrent systems. In: LNCS, vol. 1032 (1996)","DOI":"10.1007\/3-540-60761-7"},{"key":"484_CR20","unstructured":"Gomes, C., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of AAAI (1998)"},{"issue":"4","key":"484_CR21","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. Int. J. Softw. Tools Technol. Transf. 6(4), 260\u2013276 (2004)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"484_CR22","unstructured":"Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Proceedings of SPIN, LNCS, vol. 4595 (2007)"},{"issue":"10","key":"484_CR23","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"GJ Holzmann","year":"2007","unstructured":"Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Softw. Eng. 33(10), 659\u2013674 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"484_CR24","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Tackling large verification problems with the swarm tool. In: Proceedings of SPIN, LNCS, vol. 5156 (2008)","DOI":"10.1109\/ASE.2008.9"},{"key":"484_CR25","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: Proceedings of ASE, IEEE CS (2008)","DOI":"10.1109\/ASE.2008.9"},{"key":"484_CR26","doi-asserted-by":"crossref","unstructured":"Jagannath, V., Kirn, M., Lin, Y., Marinov, D.: Evaluating machine-independent metrics for state-space exploration. In: Proceedings of ICST, IEEE CS (2012)","DOI":"10.1109\/ICST.2012.112"},{"key":"484_CR27","doi-asserted-by":"crossref","unstructured":"Jones, M., Mercer, E.: Explicit state model checking with hopper. In: Proceedings of SPIN, LNCS, vol. 2989 (2004)","DOI":"10.1007\/978-3-540-24732-6_10"},{"issue":"1","key":"484_CR28","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10009-003-0115-8","volume":"7","author":"M Jones","year":"2005","unstructured":"Jones, M., Sorber, J.: Parallel search for LTL violations. Int. J. Softw. Tools Technol. Transf. 7(1), 31\u201342 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"484_CR29","doi-asserted-by":"crossref","unstructured":"Kalibera, T., Hagelberg, J., Pizlo, F., Plsek, A., Titzer, B., Vitek, J.: CDx: a family of real-time Java benchmarks. In: Proceedings of JTRES. ACM (2009)","DOI":"10.1145\/1620405.1620412"},{"key":"484_CR30","doi-asserted-by":"crossref","unstructured":"Laarman, A., Langerak, R., van de Pol, J., Weber, M., Wijs, A.: Multi-core nested depth-first search. In: Proceedings of ATVA, LNCS, vol. 6996 (2011)","DOI":"10.1007\/978-3-642-24372-1_23"},{"key":"484_CR31","unstructured":"Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Proceedings of FMCAD. IEEE (2010)"},{"key":"484_CR32","doi-asserted-by":"crossref","unstructured":"Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Proceedings of SPIN, LNCS, vol. 1680 (1999)","DOI":"10.1007\/3-540-48234-2_3"},{"issue":"4","key":"484_CR33","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0020-0190(93)90029-9","volume":"47","author":"M Luby","year":"1993","unstructured":"Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. Inf. Process. Lett. 47(4), 173\u2013180 (1993)","journal-title":"Inf. Process. Lett."},{"issue":"8","key":"484_CR34","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1109\/TSE.2006.73","volume":"32","author":"APA Moorsel van","year":"2006","unstructured":"van Moorsel, A.P.A., Wolter, K.: Analysis of restart mechanisms in software systems. IEEE Trans. Softw. Eng. 32(8), 547\u2013558 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"484_CR35","doi-asserted-by":"crossref","unstructured":"Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of PLDI. ACM (2007)","DOI":"10.1145\/1250734.1250785"},{"key":"484_CR36","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing heisenbugs in concurrent programs. In: Proceedings of OSDI, USENIX (2008)"},{"key":"484_CR37","doi-asserted-by":"crossref","unstructured":"Par\u00edzek, P., Kalibera, T.: Efficient detection of errors in Java components using random environment and restarts. In: Proceedings of TACAS, LNCS, vol. 6015 (2010)","DOI":"10.1007\/978-3-642-12002-2_37"},{"key":"484_CR38","doi-asserted-by":"crossref","unstructured":"Par\u00edzek, P., Lhot\u00e1k, O.: Randomized backtracking in state space traversal. In: Proceedings of SPIN, LNCS, vol. 6823 (2011)","DOI":"10.1007\/978-3-642-22306-8_6"},{"key":"484_CR39","doi-asserted-by":"crossref","unstructured":"Par\u00edzek, P., Lhot\u00e1k, O.: Identifying future field accesses in exhaustive state space traversal. In: Proceedings of ASE, IEEE CS (2011)","DOI":"10.1109\/ASE.2011.6100154"},{"key":"484_CR40","doi-asserted-by":"crossref","unstructured":"Par\u00edzek, P.: Hybrid analysis for partial order reduction of programs with arrays. In: Proceedings of VMCAI, LNCS, vol. 9583 (2016)","DOI":"10.1007\/978-3-662-49122-5_14"},{"key":"484_CR41","doi-asserted-by":"crossref","unstructured":"Par\u00edzek, P.: Fast error detection with hybrid analyses of future accesses. In: Proceedings of SAC, MUSEPAT Track. ACM (2016)","DOI":"10.1145\/2851613.2851935"},{"key":"484_CR42","unstructured":"Qadeer, S.: Daisy File System. Joint CAV\/ISSTA special event on specification, verification and testing of concurrent software (2004)"},{"key":"484_CR43","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Proceedings of TACAS, LNCS, vol. 3440 (2005)","DOI":"10.1007\/978-3-540-31980-1_7"},{"key":"484_CR44","doi-asserted-by":"crossref","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Proceedings of CAV, LNCS, vol. 3576 (2005)","DOI":"10.1007\/11513988_9"},{"key":"484_CR45","doi-asserted-by":"crossref","unstructured":"Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Parallel explicit model checking for generalized B\u00fcchi automata. In: Proceedings of TACAS, LNCS, vol. 9035 (2015)","DOI":"10.1007\/978-3-662-46681-0_56"},{"key":"484_CR46","unstructured":"Rungta, N., Mercer, E.: Generating counter-examples through randomized guided search. In: Proceedings of SPIN, LNCS, vol. 4595 (2007)"},{"key":"484_CR47","doi-asserted-by":"crossref","unstructured":"Rungta, N., Mercer, E.: Clash of the titans: tools and techniques for hunting bugs in concurrent programs. In: Proceedings of PADTAD. ACM (2009)","DOI":"10.1145\/1639622.1639631"},{"key":"484_CR48","doi-asserted-by":"crossref","unstructured":"Sen, K.: Effective random testing of concurrent programs. In: Proceedings of ASE. ACM (2007)","DOI":"10.1145\/1321631.1321679"},{"issue":"1\u20132","key":"484_CR49","first-page":"111","volume":"70","author":"K Seppi","year":"2006","unstructured":"Seppi, K., Jones, M., Lamborn, P.: Guided model checking with a bayesian meta-heuristic. Fundamenta Informaticae 70(1\u20132), 111\u2013126 (2006)","journal-title":"Fundamenta Informaticae"},{"key":"484_CR50","unstructured":"Smith, L.A., Bull, J.M., Obdrzalek, J.: A parallel Java grande benchmark suite. Supercomputing. ACM (2001). https:\/\/www2.epcc.ed.ac.uk\/computing\/research_activities\/java_grande\/index_1.html"},{"issue":"1","key":"484_CR51","doi-asserted-by":"publisher","first-page":"72","DOI":"10.2307\/1412159","volume":"15","author":"C Spearman","year":"1904","unstructured":"Spearman, C.: The proof and measurement of association between two things. Am. J. Psychol. 15(1), 72\u2013101 (1904)","journal-title":"Am. J. Psychol."},{"key":"484_CR52","doi-asserted-by":"crossref","unstructured":"Stern, U., Dill, D.L.: Parallelizing the murphi verifier. In: Proceedings of CAV, LNCS, vol. 1254 (1997)","DOI":"10.1007\/3-540-63166-6_26"},{"key":"484_CR53","doi-asserted-by":"crossref","unstructured":"Thomson, P., Donaldson, A.F., Betts, A.: Concurrency testing using schedule bounding: an empirical study. In: Proceedings of PPoPP. ACM (2014)","DOI":"10.1145\/2555243.2555260"},{"key":"484_CR54","doi-asserted-by":"crossref","unstructured":"Udupa, A., Desai, A., Rajamani, S.: Depth bounded explicit-state model checking. In: Proceedings of SPIN, LNCS, vol. 6823 (2011)","DOI":"10.1007\/978-3-642-22306-8_5"},{"issue":"2","key":"484_CR55","first-page":"101","volume":"25","author":"A Vargha","year":"2000","unstructured":"Vargha, A., Delaney, H.D.: A critique and improvement of the CL common language effect size statistics of McGraw and Wong. J. Educ. Behav. Stat. 25(2), 101\u2013132 (2000)","journal-title":"J. Educ. Behav. Stat."},{"key":"484_CR56","unstructured":"Walsh, T.: Search in a small world. In: Proceedings of IJCAI, Morgan Kaufmann (1999)"},{"key":"484_CR57","doi-asserted-by":"crossref","unstructured":"Wehrle, M., Kupferschmid, S., Podelski, A.: Transition-based directed model checking. In: Proceedings of TACAS, LNCS, vol. 5505 (2009)","DOI":"10.1007\/978-3-642-00768-2_19"},{"key":"484_CR58","doi-asserted-by":"crossref","unstructured":"Wehrle, M., Kupferschmid, S.: Context-enhanced directed model checking. In: Proceedings of SPIN, LNCS, vol. 6349 (2010)","DOI":"10.1007\/978-3-642-16164-3_7"},{"issue":"2","key":"484_CR59","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/s10009-015-0379-9","volume":"18","author":"A Wijs","year":"2016","unstructured":"Wijs, A., Bosnacki, D.: Many-core on-the-fly model checking of safety properties using GPUs. Int. J. Softw. Tools Technol. Transf. 18(2), 169\u2013185 (2016)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"484_CR60","doi-asserted-by":"crossref","unstructured":"Wijs, A., Lisser, B.: Distributed extended beam search for quantitative model checking. In: Proceedings of MoChArt, LNCS, vol. 4428 (2006)","DOI":"10.1007\/978-3-540-74128-2_11"},{"key":"484_CR61","unstructured":"Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: a runtime model checker for multithreaded C programs. Technical Report UUCS-08-004, University of Utah (2008)"},{"key":"484_CR62","unstructured":"Concurrency tool comparison repository, https:\/\/facwiki.cs.byu.edu\/vv-lab\/index.php\/Concurrency_Tool_Comparison"},{"key":"484_CR63","unstructured":"Java pathfinder, http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/"},{"key":"484_CR64","unstructured":"jPapaBench, http:\/\/d3s.mff.cuni.cz\/~malohlava\/projects\/jpapabench\/"},{"key":"484_CR65","unstructured":"Parallel Java benchmarks, https:\/\/bitbucket.org\/psl-lab\/pjbench"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-018-0484-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-018-0484-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-018-0484-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,13]],"date-time":"2022-08-13T13:01:10Z","timestamp":1660395670000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-018-0484-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,30]]},"references-count":65,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["484"],"URL":"https:\/\/doi.org\/10.1007\/s10009-018-0484-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,1,30]]},"assertion":[{"value":"30 January 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}