S. Bardin, P. Herrmann, and F. Perroud, An Alternative to SAT-Based Approaches for Bit-Vectors, 2010.
DOI : 10.1007/978-3-642-12002-2_7
URL : http://sebastien.bardin.free.fr/long-tacas10.pdf

S. Bardin and P. Herrmann, OSMOSE: automatic structural testing of executables, Software Testing, Verification and Reliability, vol.16, issue.1, 2011.
DOI : 10.1002/stvr.333

C. Barret, D. Dill, and J. Levitt, A decision procedure for bit-vector arithmetic, DAC 98, 1998.

C. W. Barrett, Satisfiability Modulo Theories, 2009.
DOI : 10.1007/s10817-005-5204-9
URL : https://hal.archives-ouvertes.fr/hal-01095009

A. Biere, Symbolic Model Checking without BDDs " . In: Tools and Algorithms for the Construction and Analysis of Systems, 1999.
DOI : 10.1007/3-540-49059-0_14
URL : http://repository.cmu.edu/cgi/viewcontent.cgi?article=1426&context=compsci

N. Bjørner, Taking Satisfiability to the Next Level with Z3, Proceedings of the 6th International Joint Conference on Automated Reasoning, 2012.
DOI : 10.1007/978-3-642-31365-3_1

B. Blanc, Handling State-Machines Specifications with GATeL, Electronic Notes in Theoretical Computer Science, vol.264, issue.3, 2010.
DOI : 10.1016/j.entcs.2010.12.011
URL : https://doi.org/10.1016/j.entcs.2010.12.011

R. Brinkmann and R. Drechsler, RTL-datapath verification using integer linear programming, Proceedings of ASP-DAC/VLSI Design 2002. 7th Asia and South Pacific Design Automation Conference and 15h International Conference on VLSI Design, 2002.
DOI : 10.1109/ASPDAC.2002.995022
URL : http://www.informatik.uni-bremen.de/grp/ag-ram/Paper/rtlilp.ps

R. Brummayer and A. Biere, Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays, 2009.
DOI : 10.1007/978-3-540-78800-3_24
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-642-00768-2_16.pdf

R. Bruttomesso, A Lazy and Layered SMT( $\mathcal{BV}$ ) Solver for Hard Industrial Verification Problems, Computer Aided Verification (CAV, 2007.
DOI : 10.1007/978-3-540-73368-3_54

R. E. Bryant, Deciding Bit-Vector Arithmetic with Abstraction, 2007.
DOI : 10.1007/978-3-540-71209-1_28
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-540-71209-1_28.pdf

A. Cimatti, The MathSAT5 SMT Solver, 2013.
DOI : 10.1007/978-3-642-36742-7_7

E. M. Clarke, D. Kroening, and F. Lerda, A Tool for Checking ANSI-C Programs, 2004.
DOI : 10.1007/978-3-540-24730-2_15

H. Collavizza, M. Rueher, and P. Hentenryck, CPBPV: A Constraint-Programming Framework for Bounded Program Verification, p.2008, 2008.
DOI : 10.1007/s10601-009-9089-9
URL : https://hal.archives-ouvertes.fr/hal-01099509

R. David, BINSEC/SE: A Dynamic Symbolic Execution Toolkit for Binary-Level Analysis, 2016 IEEE 23rd International Conference on Software Analysis, Evolution, and Reengineering (SANER), pp.2016-2016
DOI : 10.1109/SANER.2016.43
URL : https://hal.archives-ouvertes.fr/hal-01721502

R. Dechter, Constraint Processing, 2003.

E. W. Dijkstra, A discipline of programming, 1976.

B. Dutertre, Yices??2.2, Computer-Aided Verification (CAV), 2014.
DOI : 10.1007/978-3-319-08867-9_49

N. Eén and N. Sörensson, An Extensible SAT-solver, Theory and Applications of Satisfiability Testing, 2003.

F. Ferrandi, M. Rendine, and D. Sciuto, Functional verification for SystemC descriptions using constraint solving, Proceedings 2002 Design, Automation and Test in Europe Conference and Exhibition, 2002.
DOI : 10.1109/DATE.2002.998382
URL : http://www.sigda.org/Archives/ProceedingArchives/Date/Date2002/papers/2002/date02/htmfiles/sun_sgi/../../pdffiles/07e_2.pdf

T. Feydy, A. Schutt, and P. J. Stuckey, Global difference constraint propagation for finite domain solvers, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, 2008.
DOI : 10.1145/1389449.1389478
URL : http://www.cs.mu.oz.au/~pjs/papers/ppdp2008b.pdf

V. Ganesh and D. L. Dill, A Decision Procedure for Bit-Vectors and Arrays, 2007.
DOI : 10.1007/978-3-540-73368-3_52
URL : http://morpheus.cs.ucdavis.edu/languages/dp-vectors-arrays.pdf

P. Godefroid, Test Generation Using Symbolic Execution, 2012.

A. Gotlieb, TCAS software verification using constraint programming, The Knowledge Engineering Review, vol.99, issue.03, 2012.
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, 1998.
DOI : 10.1145/271771.271790

A. Gotlieb, M. Leconte, and B. Marre, Constraint Solving on Modular Integers, p.2010
URL : https://hal.archives-ouvertes.fr/hal-00699234

T. A. Henzinger, Lazy abstraction, 2002.
DOI : 10.1145/503272.503279

D. Kroening and O. Strichman, Decision Procedures: An Algorithmic Point of View, 2008.
DOI : 10.1007/978-3-662-50497-0

M. Leconte and B. Berstel, Extending a CP Solver with Congruences as Domains for Program Verification, Trends in Constraint Programming, 2010.
DOI : 10.1002/9780470612309.ch21
URL : http://wikix.ilog.fr/wiki/pub/Main/BrunoBerstel/cstva06.pdf

P. Manolios and D. Vroon, Efficient Circuit to CNF Conversion, 2007.
DOI : 10.1007/978-3-540-72788-0_3

B. Marre and B. Blanc, Test Selection Strategies for Lustre Descriptions in GATeL, Electronic Notes in Theoretical Computer Science, vol.111, 2005.
DOI : 10.1016/j.entcs.2004.12.010
URL : https://doi.org/10.1016/j.entcs.2004.12.010

B. Marre and C. Michel, Improving the Floating Point Addition and Subtraction Constraints, Principles and Practice of Constraint Programming -CP 2010, 2010.
DOI : 10.1007/978-3-642-15396-9_30

K. L. Mcmillan, Lazy Abstraction with Interpolants, 2006.
DOI : 10.1007/11817963_14

L. D. Michel and P. Van-hentenryck, Constraint Satisfaction over Bit-Vectors, English. In: Principles and Practice of Constraint Programming, vol.7514, 2012.
DOI : 10.1007/978-3-642-33558-7_39

R. A. Millo, R. J. Lipton, and A. J. Perlis, Social Processes and Proofs of Theorems and Programs, Communications of the Association of Computing Machinery, 1979.

M. W. Moskewicz, Chaff, Proceedings of the 38th conference on Design automation , DAC '01, 2001.
DOI : 10.1145/378239.379017

G. Nelson and D. C. Oppen, Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, 1979.
DOI : 10.1145/357073.357079
URL : http://www.cse.iitb.ac.in/~sangramraje/references/4-NelsonOppen.pdf

G. Parthasarathy, An efficient finite-domain constraint solver for circuits, Proceedings of the 41st annual conference on Design automation , DAC '04, 2004.
DOI : 10.1145/996566.996628
URL : http://www.cs.york.ac.uk/rts/docs/SIGDA-Compendium-1994-2004/papers/2004/dac04/pdffiles/p212.pdf

M. Pelleau, A Constraint Solver Based on Abstract Domains, 2013.
DOI : 10.1007/978-3-642-35873-9_26
URL : https://hal.archives-ouvertes.fr/hal-00785604

J. D. Scott, P. Flener, and J. Pearson, Bounded Strings for Constraint Programming, 2013 IEEE 25th International Conference on Tools with Artificial Intelligence, 2013.
DOI : 10.1109/ICTAI.2013.155
URL : http://www.it.uu.se/research/group/astra/publications/ICTAI13-Strings.pdf

J. P. Silva and K. A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Trans. Computers, vol.485, 1999.

A. Sülflow, Evaluation of SAT like proof techniques for formal verification of word level circuits, 8th IEEE Workshop on RTL and High Level Testing, 2007.

R. Vemuri and R. Kalyanaraman, Generation of design verification tests from behavioral VHDL programs using path enumeration and constraint programming, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol.3, issue.2, pp.201-214, 1995.
DOI : 10.1109/92.386221

W. Wang, H. Søndergaard, and P. J. Stuckey, A Bit-Vector Solver with Word-Level Propagation, 2016.
DOI : 10.1007/978-3-319-33954-2_27

N. Williams, B. Marre, and P. Mouy, On-the-fly generation of K-path tests for C functions, Proceedings. 19th International Conference on Automated Software Engineering, 2004., 2004.
DOI : 10.1109/ASE.2004.1342749
URL : http://www.lri.fr/~marre/PS/rapportASE04.pdf

Z. Zeng, M. Ciesielski, and B. Rouzeyre, Functional Test Generation Using Constraint Logic Programming, 11th Int. Conf. on Very Large Scale Integration of Systems-on-Chip, 2001.
DOI : 10.1007/3-540-63104-6_28
URL : https://hal.archives-ouvertes.fr/lirmm-00268536

Z. Zeng, P. Kalla, and M. Ciesielski, LPSAT: a unified approach to RTL satisfiability, Proceedings Design, Automation and Test in Europe. Conference and Exhibition 2001, 2001.
DOI : 10.1109/DATE.2001.915055