R. J. Anderson and H. Woll, Wait-free parallel algorithms for the union-find problem, Proceedings of the twenty-third annual ACM symposium on Theory of computing , STOC '91, pp.370-380, 1994.
DOI : 10.1145/103418.103458

J. Barnat, L. Brim, and J. Chaloupka, Parallel breadthfirst search LTL model-checking, ASE'03, pp.106-115, 2003.

J. Barnat, L. Brim, and J. Chaloupka, From Distributed Memory Cycle Detection to Parallel LTL Model Checking, FMICS'05, pp.21-39, 2005.
DOI : 10.1016/j.entcs.2004.08.056

J. Barnat, L. Brim, and P. Ro?kai, DiVinE Multi-Core ??? A Parallel LTL Model-Checker, ATVA'08, pp.234-239, 2008.
DOI : 10.1109/TSE.2007.70724

J. Barnat, L. Brim, and P. Ro?kai, A time-optimal onthe-fly parallel algorithm for model checking of weak LTL properties, ICFEM'09, pp.407-425, 2009.

J. Barnat, L. Brim, and P. Ro?kai, Scalable shared memory LTL model checking, International Journal on Software Tools for Technology Transfer, vol.39, issue.6, pp.139-153, 2010.
DOI : 10.1007/s10009-010-0136-z

M. Benedikt, R. Lenhardt, and J. Worrell, LTL Model Checking of Interval Markov Chains, TACAS'13, pp.32-46, 2013.
DOI : 10.1007/978-3-642-36742-7_3

E. D. Berger, K. S. Mckinley, R. D. Blumofe, and P. R. Wilson, Hoard: A scalable memory allocator for multithreaded applications, Journal of the ACM, pp.117-128, 2000.

I. Berman, Multicore Programming in the Face of Metamorphosis: Union-Find as an Example. Master's thesis, Tel-Aviv University, School of Computer Science, 2010. 10. V. Bloemen. On-the-fly parallel decomposition of strongly connected components, 2015.

V. Bloemen, A. Laarman, J. L. Van-de-pol-12, I. Brim, P. Cerná et al., Multi-core On-the-fly SCC Decomposition Distributed LTL model checking based on negative cycle detection Accepting predecessors are better than back edges in distributed LTL model-checking 14. I. ? Cerná and R. Pelánek. Relating hierarchy of temporal properties to model checking, PPoPP'16 FSTTCS'01 FMCAD'04 MFCS'03 SPIN'03, pp.96-107, 2001.

C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis, Memory-efficient algorithm for the verification of temporal properties, CAV'90, pp.233-242, 1991.

J. Couvreur, A. Duret-lutz, and D. Poitrenaud, On-the-fly emptiness checks for generalized Büchi automata, SPIN'05, pp.143-158, 2005.

E. W. Dijkstra, EWD 376: Finding the maximum strong components in a directed graph, 1973.

A. Duret-lutz and D. Poitrenaud, SPOT: an extensible model checking library using transition-based generalized buchi automata, The IEEE Computer Society's 12th Annual International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems, 2004. (MASCOTS 2004). Proceedings., pp.76-83, 2004.
DOI : 10.1109/MASCOT.2004.1348184
URL : https://hal.archives-ouvertes.fr/hal-01496158

S. Evangelista, L. Petrucci, and S. Youcef, Parallel Nested Depth-First Searches for LTL Model Checking, ATVA'11, pp.381-396, 2011.
DOI : 10.1007/978-3-642-24372-1_27

S. Evangelista, A. Laarman, L. Petrucci, and J. Van, Improved Multi-Core Nested Depth-First Search, ATVA'12, pp.269-283, 2012.
DOI : 10.1007/978-3-642-33386-6_22

A. Gaiser and S. Schwoon, Comparison of algorithms for checking emptiness on Büchi automata, MEMICS'09, 2009.

G. J. Holzmann, R. Joshi, and A. Groce, Swarm Verification Techniques, IEEE Transactions on Software Engineering, vol.37, issue.6, pp.845-857, 2011.
DOI : 10.1109/TSE.2010.110

G. Kant, A. W. Laarman, J. J. Meijer, J. C. Van-de-pol, S. C. Blom et al., LTSmin: High-Performance Language-Independent Model Checking, Tools and Algorithms for the Construction and Analysis of Systems, pp.692-707, 2015.
DOI : 10.1007/978-3-662-46681-0_61

Y. Kesten, A. Pnueli, and L. On-raviv, Algorithmic verification of linear temporal logic specifications, ICALP'98, pp.1-16, 1998.
DOI : 10.1007/BFb0055036

A. Laarman and J. Van, Variations on multicore nested depth-first search, PDMC'11, pp.13-28, 2011.

A. Laarman, R. Langerak, J. Van-de-pol, M. Weber, and A. Wijs, Multi-core nested depth-first search, ATVA'11, pp.321-335, 2011.
DOI : 10.1007/978-3-642-24372-1_23
URL : http://eprints.eemcs.utwente.nl/20337/01/mcndfs.pdf

G. Lowe, Concurrent depth-first search algorithms based on Tarjan???s Algorithm, International Journal on Software Tools for Technology Transfer, vol.1, issue.2, pp.1-19, 2015.
DOI : 10.1007/s10009-015-0382-1

M. M. Michael and M. L. Scott, Simple, fast, and practical non-blocking and blocking concurrent queue algorithms, Proceedings of the fifteenth annual ACM symposium on Principles of distributed computing , PODC '96, pp.267-275, 1996.
DOI : 10.1145/248052.248106

E. Nuutila and E. Soisalon-soininen, On finding the strongly connected components in a directed graph, Information Processing Letters, vol.49, issue.1, pp.9-14, 1994.
DOI : 10.1016/0020-0190(94)90047-7

M. M. Patwary, J. R. Blair, and F. Manne, Experiments on Union-Find Algorithms for the Disjoint-Set Data Structure, SEA'10, pp.411-423, 2010.
DOI : 10.1007/978-3-642-13193-6_35

R. Pelánek, BEEM: Benchmarks for Explicit Model Checkers, SPIN'07, pp.263-267, 2007.
DOI : 10.1007/978-3-540-73370-6_17

R. Pelánek, Properties of state spaces and their applications, International Journal on Software Tools for Technology Transfer, vol.298, issue.5594, pp.443-454, 2008.
DOI : 10.1007/s10009-008-0070-5

J. H. Reif, Depth-first search is inherently sequential, Information Processing Letters, vol.20, issue.5, pp.229-234, 1985.
DOI : 10.1016/0020-0190(85)90024-9

E. Renault, A. Duret-lutz, F. Kordon, and D. Poitrenaud, Three SCC-based emptiness checks for generalized Büchi automata, LPAR'13, pp.668-682, 2013.

E. Renault, A. Duret-lutz, F. Kordon, and D. , Poitre- naud. Strength-based decomposition of the property Büchi automaton for faster model checking, TACAS'13, pp.580-593, 2013.

E. Renault, A. Duret-lutz, F. Kordon, and D. Poitrenaud, Parallel explicit model checking for generalized Büchi automata, TACAS'15, pp.613-627, 2015.

S. Schwoon and J. Esparza, A Note on On-the-Fly Verification Algorithms, TACAS'05, 2005.
DOI : 10.1007/978-3-540-31980-1_12

R. Tarjan, Depth-First Search and Linear Graph Algorithms, SIAM Journal on Computing, vol.1, issue.2, pp.146-160, 1972.
DOI : 10.1137/0201010

R. E. Tarjan, Efficiency of a Good But Not Linear Set Union Algorithm, Journal of the ACM, vol.22, issue.2, pp.215-225, 1975.
DOI : 10.1145/321879.321884

H. Tauriainen, Nested emptiness search for generalized Büchi automata, ACSD'04, pp.165-174, 2004.