C. Baier and J. P. Katoen, Principles of Model Checking, 2008.

V. Bloemen, A. Laarman, and J. Van-de-pol, Multi-core on-the-fly SCC decomposition, PPoPP'16, pp.1-8, 2016.

V. Bloemen, A. Duret-lutz, and J. Van-de-pol, Explicit state model checking with generalized Büchi and Rabin automata. In: SPIN'17: Model Checking of Software, 2017.
DOI : 10.1145/3092282.3092288

J. R. Burch, E. M. Clarke, K. L. Mcmillan, D. L. Dill, and L. J. Hwang, Symbolic model checking: 10/sup 20/ states and beyond, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.142-170, 1992.
DOI : 10.1109/LICS.1990.113767

C. Courcoubetis, M. Y. Vardi, P. Wolper, and M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design, vol.64, issue.12, pp.275-288, 1992.
DOI : 10.1007/3-540-51803-7_23

T. Van-dijk and J. Van-de-pol, Sylvan: multi-core framework for decision diagrams, International Journal on Software Tools for Technology Transfer, vol.3, issue.2, 2016.
DOI : 10.1145/263764.263784

E. W. Dijkstra, A Discipline of Programming, 1976.

G. Kant, A. Laarman, J. Meijer, J. Van-de-pol, S. Blom et al., LTSmin: High-Performance Language-Independent Model Checking, TACAS 2015, pp.692-707, 2015.
DOI : 10.1007/978-3-662-46681-0_61

A. Laarman, E. Pater, J. Van-de-pol, and H. Hansen, Guard-based partial-order reduction, International Journal on Software Tools for Technology Transfer, vol.40, issue.1, pp.427-448, 2016.
DOI : 10.1090/dimacs/029/12
URL : http://wwwhome.cs.utwente.nl/~laarman/papers/guard-based-por.pdf

A. Laarman, J. Van-de-pol, and M. Weber, Boosting multi-core reachability performance with shared hash tables, pp.247-255, 2010.

A. W. Laarman, M. C. Olesen, A. E. Dalsgaard, K. G. Larsen, and J. C. Van-de-pol, Multi-core emptiness checking of timed Büchi automata using inclusion abstraction, CAV 2013, pp.968-983, 2013.

W. Oortwijn, T. Van-dijk, and J. Van-de-pol, Distributed binary decision diagrams for symbolic reachability, Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software , SPIN 2017, 2017.
DOI : 10.1145/155332.155354

A. Valmari, A stubborn attack on state explosion, Formal Methods in System Design, vol.31, issue.3, pp.297-322, 1992.
DOI : 10.1007/3-540-55179-4_32

. Abstract, computing systems rely on distributed, partitioned, and replicated data stores Such cloud storage systems are complex software artifacts that are very hard to design and analyze. Formal specification and model checking should therefore be beneficial during their design and validation. In particular, I propose rewriting logic and its accompanying Maude tools as a suitable framework for formally specifying and analyzing both the correctness and the performance of cloud storage systems. This abstract of an invited talk gives a short overview of the use of rewriting logic at the University of Illinois' Assured Cloud Computing center on industrial data stores such as Google's Megastore and Facebook/Apache's Cassandra. I also briefly summarize the experiences of the use of a different formal method for similar purposes by engineers at Amazon Web Services, Contents Invited Talk Design and Validation of Cloud Storage Systems Using Formal Methods. . . . 3

S. Hanifehnezhad, A. Dolati, and .. , Inverse Multi-objective Shortest Path Problem Under the Bottleneck Type Weighted Hamming Distance, p.34

M. Karimi, M. Aman, and .. , and Ardeshir Dolati Locality-Based Relaxation: An Efficient Method for GPU-Based Computation of Shortest Paths, p.41

M. Safari, A. Ebnenasir-logic-automata, and .. , Semantics, and Programming Theory Exposing Latent Mutual Exclusion by Work, p.59

T. , R. Mousavi, J. Sgall-author-index, and .. , 106 Alimujiang Yasen and Kazunori Ueda Erratum to: Topics in Theoretical Computer Science, p.125