R. Alur and D. 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

M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry et al., A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, CPP, pp.135-150, 2011.
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130

C. Ballabriga, H. Cassé, C. Rochange, and P. Sainrat, OTAWA: An Open Toolbox for Adaptive WCET Analysis, Software Technologies for Future Embedded and Ubiquitous Systems (SEUS), 2010.
DOI : 10.1007/978-3-642-16256-5_6
URL : https://hal.archives-ouvertes.fr/hal-01055378

J. Béchennec and F. Cassez, Computation of wcet using program slicing and real-time model-checking, 2011.

N. Beldiceanu, M. Carlsson, S. Demassey, and T. Petit, Global Constraint Catalogue: Past, Present and Future, Constraints, vol.2, issue.1, pp.21-62, 2007.
DOI : 10.1007/s10601-006-9010-8
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.102.251

Y. Bertot and P. Casteran, Interactive Theorem Proving and Program Development, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

A. Dalsgaard, M. Olesen, M. Toft, R. Hansen, and K. Larsen, METAMOC: Modular execution time analysis using model checking, 10th International Workshop on Worst-Case Execution Time Analysis (WCET), 2010.

A. Fauth, J. Van-praet, and M. Freericks, Describing instruction set processors using nML, Proceedings the European Design and Test Conference. ED&TC 1995, 1995.
DOI : 10.1109/EDTC.1995.470354
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.409.3477

M. Freericks, The nml machine description formalism, 1991.

H. Herbegue, H. Cassé, M. Filali, and C. Rochange, Hardware architecture specification and constraint-based WCET computation, 2013 8th IEEE International Symposium on Industrial Embedded Systems (SIES), 2013.
DOI : 10.1109/SIES.2013.6601499
URL : https://hal.archives-ouvertes.fr/hal-01148073

C. Hoare, Communicating Sequential Processes, 1985.

X. Li, A. Roychoudhury, and T. Mitra, Modeling out-of-order processors for WCET analysis. Real-Time Systems, 2006.

P. Mishra and N. Dutt, Modeling and validation of pipeline specifications, ACM Transactions on Embedded Computing Systems, vol.3, issue.1, pp.114-139, 2004.
DOI : 10.1145/972627.972633

T. Nipkow, L. Paulson, M. Wenzel, /. Isabelle, and . Hol, A Proof Assistant for Higher-Order Logic. Number 2283 in Lecture Notes in Computer Science, 2002.

V. Rajesh and R. Moona, Processor modeling for hardware software codesign, Proceedings Twelfth International Conference on VLSI Design. (Cat. No.PR00013), 2000.
DOI : 10.1109/ICVD.1999.745137

C. Rochange and P. Sainrat, A context-parameterized model for static analysis of execution times. Transactions on High-Performance Embedded Architectures and Compilers II, 2009.

R. Wilhelm, J. Engblom, A. Ermedahl, N. Holsti, S. Thesing et al., The worst-case execution-time problem???overview of methods and survey of tools, TECS), 2008.
DOI : 10.1145/1347375.1347389