E. Albert, M. Gómez-zamalloa, and G. Puebla, Test Data Generation of Bytecode by CLP Partial Evaluation, LOPSTR 2008, pp.4-23, 2008.
DOI : 10.1145/267580.267590

M. Barnett, K. Rustan, and M. Leino, Weakest- Precondition of Unstructured Programs, Information Processing Letters, vol.93, issue.6, pp.281-288

T. Bochot, P. Virelizier, V. Héì-ene-waeselynck, and . Wiels, Model checking flight control systems: The Airbus experience, 2009 31st International Conference on Software Engineering, Companion Volume, pp.18-27, 2009.
DOI : 10.1109/ICSE-COMPANION.2009.5070960

B. Botella, A. Gotlieb, and C. Michel, Symbolic execution of floating-point computations, Software Testing, Verification and Reliability, vol.14, issue.2, pp.97-121, 2006.
DOI : 10.1002/stvr.333

URL : https://hal.archives-ouvertes.fr/inria-00540299

A. Coen-porisini, G. Denaro, C. Ghezzi, and M. Pezzè, Using symbolic execution for verifying safety-critical systems, ESEC / SIG- SOFT FSE, pp.142-151, 2001.

C. Héì-ene and M. Rueher, Exploration of the capabilities of constraint programming for software verification, TACAS, pp.182-196, 2006.

M. Héì-ene-collavizza, P. Rueher, and . Van-hentenryck, CPBPV : A Constraint-Programming Framework for Bounded Program Verification, CP 2008, pp.327-341, 2008.

M. Héì-ene-collavizza, P. Rueher, and . Van-hentenryck, CPBPV: a constraint-programming framework for bounded program verification, Constraints, vol.404, issue.3, pp.238-264, 2010.
DOI : 10.1007/s10601-009-9089-9

R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck, Efficiently computing static single assignment form and the control dependence graph, ACM Transactions on Programming Languages and Systems, vol.13, issue.4, pp.451-490, 1991.
DOI : 10.1145/115372.115320

T. Denmat, A. Gotlieb, and M. Ducassé, Improving Constraint-Based Testing with Dynamic Linear Relaxations, The 18th IEEE International Symposium on Software Reliability (ISSRE '07), pp.181-190, 2006.
DOI : 10.1109/ISSRE.2007.34

URL : https://hal.archives-ouvertes.fr/hal-00180513

D. Vijay, D. Silva, G. Kroening, and . Weissenbacher, A survey of automated techniques for formal software verification, IEEE Trans. on CAD of Integrated Circuits and Systems, vol.27, issue.7, pp.1165-1178, 2008.

G. Fraser, F. Wotawa, and P. Ammann, Testing with model checkers: a survey, Software Testing, Verification and Reliability, vol.1, issue.1-2, pp.215-261, 2009.
DOI : 10.1109/MTV.2006.10

P. Godefroid, N. Klarlund, and K. Sen, Dart : directed automated random testing, PLDI, pp.213-223, 2005.

A. Gotlieb, Euclide: A Constraint-Based Testing Framework for Critical C Programs, 2009 International Conference on Software Testing Verification and Validation, pp.151-160, 2009.
DOI : 10.1109/ICST.2009.10

A. Gotlieb, TCAS software verification using constraint programming, The Knowledge Engineering Review, vol.99, issue.03, 2010.
DOI : 10.1109/TSE.2004.22

URL : https://hal.archives-ouvertes.fr/hal-00807905

A. Gotlieb, B. Botella, and M. Rueher, Automatic test data generation using constraint solving techniques, ISSTA, pp.53-62, 1998.
DOI : 10.1145/271771.271790

P. Herber, F. Friedemann, and S. Glesner, Combining Model Checking and Testing in a Continuous HW/SW Co-verification Process, TAP 2009, pp.121-136, 2009.
DOI : 10.1007/978-3-540-73370-6_14

D. Jackson and M. Vazir, Finding bugs with a constraint solver, ISSTA, pp.14-25, 2000.

C. Livadas, J. Lygeros, and N. A. Lynch, High-level modeling and analysis of TCAS, Proceedings 20th IEEE Real-Time Systems Symposium (Cat. No.99CB37054), pp.115-125, 1999.
DOI : 10.1109/REAL.1999.818833

N. Williams, B. Marre, P. Mouy, and M. Roger, PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis, Dependable Computing -EDCC'05, pp.281-292, 2005.
DOI : 10.1007/11408901_21

T. Nguyen, Y. Sy, and . Deville, Automatic test data generation for programs with integer and float variables, ASE, pp.13-21, 2001.