R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

R. Alur, Timed automata, LNCS, vol.1633, pp.8-22, 1999.
DOI : 10.1007/978-3-642-59615-5_12

J. Bengtsson and W. Yi, Timed automata: Semantics, algorithms and tools. In: Lectures on Concurrency and Petri Nets, LNCS, vol.3098, pp.87-124, 2003.
DOI : 10.1007/978-3-540-27755-2_3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.332.8701

G. Behrmann, A. David, and K. G. Larsen, A Tutorial on Uppaal, LNCS, vol.3185, pp.200-236, 2004.
DOI : 10.1007/978-3-540-30080-9_7

G. Behrmann, K. G. Larsen, J. Pearson, C. Weise, and W. Yi, Efficient timed reachability analysis using clock difference diagrams, LNCS, vol.1633, pp.341-353, 1999.
DOI : 10.7146/brics.v5i47.19492
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.16.4832

D. Beyer and A. Noack, Can Decision Diagrams Overcome State Space Explosion in Real-Time Verification?, LNCS, vol.1, issue.1-2, pp.193-208, 2003.
DOI : 10.1007/3-540-65193-4_20

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, Symbolic Model Checking without BDDs, LNCS, vol.1579, pp.193-207, 1999.
DOI : 10.1007/3-540-49059-0_14
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.8033

B. Wo´znawo´zna, A. Zbrzezny, and W. Penczek, Checking reachability properties for timed automata via SAT, Fundamenta Informatica, vol.55, issue.2, pp.223-241, 2003.

M. Sorea, Bounded model checking for timed automata, Electronic Notes in Theoretical Computer Science, vol.68, issue.5, 2002.

G. Audemard, A. Cimatti, A. Kornilowicz, and R. Sebastiani, Bounded Model Checking for Timed Systems, LNCS, vol.2529, pp.243-259, 2002.
DOI : 10.1007/3-540-36135-9_16
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.2.4600

J. Malinowski and P. Niebert, SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata, TACAS 2010, pp.405-419, 2010.
DOI : 10.1007/978-3-642-12002-2_34

R. Kindermann, T. Junttila, and I. Niemelä, Modeling for Symbolic Analysis of Safety Instrumented Systems with Clocks, 2011 Eleventh International Conference on Application of Concurrency to System Design, pp.185-194, 2011.
DOI : 10.1109/ACSD.2011.29

C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli, Satisfiability modulo theories. In: Handbook of Satisfiability, pp.825-885, 2009.
URL : https://hal.archives-ouvertes.fr/hal-01095009

A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore et al., NuSMV 2: An OpenSource Tool for Symbolic Model Checking, LNCS, vol.2404, pp.359-364, 2002.
DOI : 10.1007/3-540-45657-0_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.107.8023

A. Biere, K. Heljanko, T. Junttila, T. Latvala, and V. Schuppan, Linear Encodings of Bounded LTL Model Checking, Logical Methods in Computer Science, vol.2, issue.5, pp.5-6, 2006.
DOI : 10.2168/LMCS-2(5:5)2006
URL : http://arxiv.org/pdf/cs.LO/0611029

B. Dutertre and L. M. De-moura, A Fast Linear-Arithmetic Solver for DPLL(T), LNCS, vol.4144, pp.81-94, 2006.
DOI : 10.1007/11817963_11
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.92.705

E. M. Clarke, D. Kroening, J. Ouaknine, and O. Strichman, Completeness and Complexity of Bounded Model Checking, LNCS, vol.2937, pp.85-96, 2004.
DOI : 10.1007/978-3-540-24622-0_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.11.1380

S. Tripakis, S. Yovine, and A. Bouajjani, Checking Timed B??chi Automata Emptiness Efficiently, Formal Methods in System Design, vol.18, issue.1, pp.267-292, 2005.
DOI : 10.1007/s10703-005-1632-8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.65.7565

K. G. Larsen, P. Pettersson, and W. Yi, Model-checking for real-time systems, LNCS, vol.965, pp.62-88, 1995.
DOI : 10.1007/3-540-60249-6_41

J. Lahtinen, K. Björkman, J. Valkonen, J. Frits, and I. Niemelä, Analysis of an emergency diesel generator control system by compositional model checking, VTT Working Papers, vol.156, 2010.