Fast detection of concurrency errors by state space traversal with randomization and early backtracking

Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. In: Proceedings of POPL. ACM (2014)

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–1288 (2012)

Behrmann, G., Hune, T., Vaandrager, F.: Distributing timed model checking—how the search order matters. In: Proceedings of CAV, LNCS, vol. 1855 (2000)

Biere, A.: PicoSAT essentials. J. Satisf. Boolean Model. Comput. (JSAT) 4, 75–97 (2008)

Bisiani, R.: Beam Search. Encyclopedia of Artificial Intelligence. Wiley, New York (1992)

Burckhardt, S., Kothari, P., Musuvathi, M., Nagarakatte, S.: A Randomized scheduler with probabilistic guarantees of finding bugs. In: Proceedings of ASPLOS. ACM (2010)

Ciardo, G., Gluckman, J., Nicol, D.: Distributed state space generation of discrete-state stochastic models. INFORMS J. Comput. 10(1), 82–93 (1998)

Coons, K.E., Burckhardt, S., Musuvathi, M.: GAMBIT: effective unit testing for concurrency libraries. In: Proceedings of PPoPP. ACM (2010)

Dwyer, M.B., Elbaum, S.G., Person, S., Purandare, R.: Parallel randomized state-space search. In: Proceedings of ICSE, IEEE CS (2007)

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–3), 199–240 (2004)

Dwyer, M.B., Person, S., Elbaum, S.G.: Controlling factors in evaluating path-sensitive error detection techniques. In: Proceedings of SIGSOFT FSE. ACM (2006)

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–3), 247–267 (2004)

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)

Een, N., Sorensson, N.: An extensible SAT-solver. In: Proceedings of SAT, LNCS, vol. 2919 (2003)

Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded scheduling. In: Proceedings of POPL. ACM (2011)

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–287 (2009)

Farzan, A., Holzer, A., Razavi, N., Veith, H.: Con2colic testing. In: Proceedings of ESEC/FSE. ACM (2013)

Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of POPL. ACM (2005)

Godefroid, P.: Partial-order methods for the verification of concurrent systems. In: LNCS, vol. 1032 (1996)

Gomes, C., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: Proceedings of AAAI (1998)

Groce, A., Visser, W.: Heuristics for model checking Java programs. Int. J. Softw. Tools Technol. Transf. 6(4), 260–276 (2004)

Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Proceedings of SPIN, LNCS, vol. 4595 (2007)

Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Softw. Eng. 33(10), 659–674 (2007)

Holzmann, G.J., Joshi, R., Groce, A.: Tackling large verification problems with the swarm tool. In: Proceedings of SPIN, LNCS, vol. 5156 (2008)

Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification. In: Proceedings of ASE, IEEE CS (2008)

Jagannath, V., Kirn, M., Lin, Y., Marinov, D.: Evaluating machine-independent metrics for state-space exploration. In: Proceedings of ICST, IEEE CS (2012)

Jones, M., Mercer, E.: Explicit state model checking with hopper. In: Proceedings of SPIN, LNCS, vol. 2989 (2004)

Jones, M., Sorber, J.: Parallel search for LTL violations. Int. J. Softw. Tools Technol. Transf. 7(1), 31–42 (2005)

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)

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)

Laarman, A., van de Pol, J., Weber, M.: Boosting multi-core reachability performance with shared hash tables. In: Proceedings of FMCAD. IEEE (2010)

Lerda, F., Sisto, R.: Distributed-memory model checking with SPIN. In: Proceedings of SPIN, LNCS, vol. 1680 (1999)

Luby, M., Sinclair, A., Zuckerman, D.: Optimal speedup of Las Vegas algorithms. Inf. Process. Lett. 47(4), 173–180 (1993)

van Moorsel, A.P.A., Wolter, K.: Analysis of restart mechanisms in software systems. IEEE Trans. Softw. Eng. 32(8), 547–558 (2006)

Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: Proceedings of PLDI. ACM (2007)

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)

Parízek, P., Kalibera, T.: Efficient detection of errors in Java components using random environment and restarts. In: Proceedings of TACAS, LNCS, vol. 6015 (2010)

Parízek, P., Lhoták, O.: Randomized backtracking in state space traversal. In: Proceedings of SPIN, LNCS, vol. 6823 (2011)

Parízek, P., Lhoták, O.: Identifying future field accesses in exhaustive state space traversal. In: Proceedings of ASE, IEEE CS (2011)

Parízek, P.: Hybrid analysis for partial order reduction of programs with arrays. In: Proceedings of VMCAI, LNCS, vol. 9583 (2016)

Parízek, P.: Fast error detection with hybrid analyses of future accesses. In: Proceedings of SAC, MUSEPAT Track. ACM (2016)

Qadeer, S.: Daisy File System. Joint CAV/ISSTA special event on specification, verification and testing of concurrent software (2004)

Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Proceedings of TACAS, LNCS, vol. 3440 (2005)

Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Proceedings of CAV, LNCS, vol. 3576 (2005)

Renault, E., Duret-Lutz, A., Kordon, F., Poitrenaud, D.: Parallel explicit model checking for generalized Büchi automata. In: Proceedings of TACAS, LNCS, vol. 9035 (2015)

Rungta, N., Mercer, E.: Generating counter-examples through randomized guided search. In: Proceedings of SPIN, LNCS, vol. 4595 (2007)

Rungta, N., Mercer, E.: Clash of the titans: tools and techniques for hunting bugs in concurrent programs. In: Proceedings of PADTAD. ACM (2009)

Sen, K.: Effective random testing of concurrent programs. In: Proceedings of ASE. ACM (2007)

Seppi, K., Jones, M., Lamborn, P.: Guided model checking with a bayesian meta-heuristic. Fundamenta Informaticae 70(1–2), 111–126 (2006)

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

Spearman, C.: The proof and measurement of association between two things. Am. J. Psychol. 15(1), 72–101 (1904)

Stern, U., Dill, D.L.: Parallelizing the murphi verifier. In: Proceedings of CAV, LNCS, vol. 1254 (1997)

Thomson, P., Donaldson, A.F., Betts, A.: Concurrency testing using schedule bounding: an empirical study. In: Proceedings of PPoPP. ACM (2014)

Udupa, A., Desai, A., Rajamani, S.: Depth bounded explicit-state model checking. In: Proceedings of SPIN, LNCS, vol. 6823 (2011)

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–132 (2000)

Walsh, T.: Search in a small world. In: Proceedings of IJCAI, Morgan Kaufmann (1999)

Wehrle, M., Kupferschmid, S., Podelski, A.: Transition-based directed model checking. In: Proceedings of TACAS, LNCS, vol. 5505 (2009)

Wehrle, M., Kupferschmid, S.: Context-enhanced directed model checking. In: Proceedings of SPIN, LNCS, vol. 6349 (2010)

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–185 (2016)

Wijs, A., Lisser, B.: Distributed extended beam search for quantitative model checking. In: Proceedings of MoChArt, LNCS, vol. 4428 (2006)

Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: a runtime model checker for multithreaded C programs. Technical Report UUCS-08-004, University of Utah (2008)

Concurrency tool comparison repository, https://facwiki.cs.byu.edu/vv-lab/index.php/Concurrency_Tool_Comparison

Java pathfinder, http://babelfish.arc.nasa.gov/trac/jpf/

jPapaBench, http://d3s.mff.cuni.cz/~malohlava/projects/jpapabench/

Parallel Java benchmarks, https://bitbucket.org/psl-lab/pjbench