M. N. Bowen-alpern, F. K. Wegman, and . Zadeck, Detecting equality of variables in programs, Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.1-11, 1988.

R. Brummayer and A. Biere, Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays, Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software TACAS '09, pp.174-177, 2009.
DOI : 10.1007/978-3-540-78800-3_24

A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, Bounded Model Checking, of Advances in Computers, pp.117-148, 2003.
DOI : 10.1016/S0065-2458(03)58003-2

J. Becker and O. Sander, Automotive, Railway and Avionics Multicore Systems -ARAMiS

P. Cousot and R. Cousot, Abstract interpretation, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '77, pp.238-252, 1977.
DOI : 10.1145/512950.512973

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

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min et al., The ASTRE?? Analyzer, Programming Languages and Systems, Proceedings of the 14th European Symposium on Programming, pp.21-30, 2005.
DOI : 10.1007/978-3-540-31987-0_3

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-Guided Abstraction Refinement, Computer Aided Verification, pp.154-169, 2000.
DOI : 10.1007/10722167_15

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=

[. Clarke, D. Kroening, and F. Lerda, A Tool for Checking ANSI-C Programs, Tools and Algorithms for the Construction and Analysis of Systems, pp.168-176, 2004.
DOI : 10.1007/978-3-540-24730-2_15

L. Mendonça-de-moura and N. Bjørner, Z3: An Efficient SMT Solver, TACAS, pp.337-340, 2008.

L. De, M. , and N. Bjørner, Satisfiability Modulo Theories: An Appetizer, Formal Methods: Foundations and Applications, pp.23-36, 2009.

[. En and N. Srensson, An Extensible SAT-solver, Lecture Notes in Computer Science, vol.2919, pp.502-518, 2003.
DOI : 10.1007/978-3-540-24605-3_37

C. Fht-+-07-]-martin-fränzle, T. Herde, S. Teige, T. Ratschan, and . Schubert, Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure, Journal on Satisfiability Boolean Modeling and Computation, vol.1, pp.209-236, 2007.

C. Lattner and V. Adve, LLVM: A compilation framework for lifelong program analysis & transformation, International Symposium on Code Generation and Optimization, 2004. CGO 2004., 2004.
DOI : 10.1109/CGO.2004.1281665

J. R. Levine, Linkers and Loaders, 1999.

M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik, Chaff, Proceedings of the 38th conference on Design automation , DAC '01, pp.530-535, 2001.
DOI : 10.1145/378239.379017

D. Nowotka and J. Traub, MEMICS -Memory Interval Constrain Solving of (concurrent) Machine Code, Automotive -Safety & Security 2012: Sicherheit und Zuverlässigkeit für automobile Informationstechnik, pp.69-83, 2012.

A. Raza, G. Vogel, and E. Plödereder, Bauhaus ??? A Tool Suite for Program Analysis and Reverse Engineering, Reliable Software Technologies -Ada-Europe, pp.71-82, 2006.
DOI : 10.1007/11767077_6

K. Barry, M. N. Rosen, F. K. Wegman, and . Zadeck, Global value numbers and redundant computations, Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.12-27, 1988.

[. Sinz, S. Falke, and F. Merz, A Precise Memory Model for Low- Level Bounded Model Checking, Proceedings of the 5th International Workshop on Systems Software Verification (SSV '10), 2010.

[. Sweetman, See MIPS Run, Second Edition, 2006.

[. Weiser, Program Slicing, Proceedings of the 5th international conference on Software engineering, ICSE '81, pp.439-449, 1981.
DOI : 10.1109/TSE.1984.5010248