R. Alur, T. Dang, and F. Ivancic, Predicate abstraction for reachability analysis of hybrid systems, ACM Transactions on Embedded Computing Systems, vol.5, issue.1, pp.152-199, 2006.
DOI : 10.1145/1132357.1132363

G. Audemard, M. Bozzano, A. Cimatti, and R. Sebastiani, Verifying Industrial Hybrid Systems with MathSAT, Electronic Notes in Theoretical Computer Science, vol.119, issue.2, pp.17-32, 2005.
DOI : 10.1016/j.entcs.2004.12.022
URL : https://hal.archives-ouvertes.fr/hal-00396426

J. Bengtsson, B. Jonsson, J. Lilius, and W. Yi, Partial order reductions for timed systems, CONCUR, volume 1466 of LNCS, pp.485-500, 1998.
DOI : 10.1007/BFb0055643

R. Bruttomesso, A. Cimatti, A. Franzén, A. Griggio, and R. Sebastiani, The MathSAT??4 SMT Solver, CAV, pp.299-303, 2008.
DOI : 10.1007/978-3-540-70545-1_28

L. Bu and X. Li, Path-Oriented Bounded Reachability Analysis of Compositional Linear Hybrid Systems, manuscript submitted, 2008.

L. Bu, Y. Li, L. Wang, X. Chen, and X. Li, BACH2: Bounded reachAbility CHecker for Compositional Linear Hybrid Systems, DATE, pp.1512-1517, 2010.

A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore et al., NuSMV 2: An OpenSource Tool for Symbolic Model Checking, CAV, volume 2102 of LNCS, pp.359-364, 2002.
DOI : 10.1007/3-540-45657-0_29

M. Fränzle and C. Herde, Efficient Proof Engines for Bounded Model Checking of Hybrid Systems, Electronic Notes in Theoretical Computer Science, vol.133, pp.119-137, 2005.
DOI : 10.1016/j.entcs.2004.08.061

M. Fränzle and C. Herde, HySAT: An efficient proof engine for bounded model checking of hybrid systems, Formal Methods in System Design, vol.68, issue.2, pp.179-198, 2007.
DOI : 10.1007/s10703-006-0031-0

N. Giorgetti, G. J. Pappas, and A. Bemporad, Bounded Model Checking of Hybrid Dynamical Systems, Proceedings of the 44th IEEE Conference on Decision and Control, pp.672-677, 2005.
DOI : 10.1109/CDC.2005.1582233

P. Godefroid, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, LNCS, vol.1032, 1996.
DOI : 10.1007/3-540-60761-7

K. Heljanko and I. Niemelä, Bounded LTL model checking with stable models, Theory and Practice of Logic Programming, pp.519-550, 2003.

T. A. Henzinger, The theory of hybrid automata, Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, pp.278-292, 1996.
DOI : 10.1109/LICS.1996.561342

S. Jha, B. Krogh, J. Weimer, and E. Clarke, Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction, HSCC, pp.287-300, 2007.
DOI : 10.1007/978-3-540-71493-4_24
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.72.2143

R. Sebastiani, Lazy satisability modulo theories, JSAT, vol.3, pp.3-4141, 2007.

U. Shinya, Event order abstraction for parametric real-time system verification, EMSOFT, pp.1-10, 2008.

C. Wang, Z. Yang, V. Kahlon, and A. Gupta, Peephole Partial Order Reduction, TACAS, pp.382-396, 2008.
DOI : 10.1007/978-3-540-78800-3_29
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.128.8845

F. Wang, Symbolic Parametric Safety Analysis of Linear Hybrid Systems with BDD-Like Data-Structures, IEEE Trans. Soft. Eng, vol.31, issue.1, pp.38-51, 2005.
DOI : 10.1007/978-3-540-27813-9_23

J. Zhao, X. Li, T. Zheng, and G. Zheng, Removing Irrelevant Atomic Formulas for Checking Timed Automata Efficiently, FORMATS, volume 2791 of LNCS, pp.34-45, 2003.
DOI : 10.1007/978-3-540-40903-8_4