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