R. Baldoni, E. Coppa, D. Cono-d'elia, C. Demetrescu, and I. Finocchi, A survey of symbolic execution techniques, ACM Comput. Surv, vol.51, issue.3, 2018.

M. Barnett, -. Bor, R. Chang, B. Deline, K. Jacobs et al., Boogie: A modular reusable verifier for object-oriented programs, FMCO, vol.4111, pp.364-387, 2005.

M. Barnett, M. Fähndrich, K. Rustan, M. Leino, P. Müller et al., Specification and verification: the Spec# experience, Commun. ACM, vol.54, issue.6, pp.81-91, 2011.

A. Biere, A. Cimatti, E. M. Clarke, O. Strichman, and Y. Zhu, Bounded model checking, Advances in Computers, vol.58, pp.117-148, 2003.

S. Chatterjee, K. Shuvendu, S. Lahiri, Z. Qadeer, and . Rakamaric, A reachability predicate for analyzing low-level software, TACAS, vol.4424, pp.19-33, 2007.

E. M. Clarke, D. Kroening, and F. Lerda, A tool for checking ANSI-C programs, TACAS, vol.2988, pp.168-176, 2004.

A. Stephen and . Cook, Soundness and completeness of an axiom system for program verification, SIAM J. Comput, vol.7, issue.1, pp.70-90, 1978.

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 Trans. Program. Lang. Syst, vol.13, issue.4, pp.451-490, 1991.

J. Stijn-de-gouw and . Rot, Effectively eliminating auxiliaries, Theory and Practice of Formal Methods, vol.9660, pp.226-241, 2016.

D. L. Detlefs, K. Rustan, M. Leino, G. Nelson, and J. B. Saxe, Extended static checking, Research report, vol.159, 1998.

W. Edsger and . Dijkstra, A Discipline of Programming, 1976.

J. , C. Filliâtre, and A. Paskevich, Why3 -where programs meet provers, ESOP, vol.7792, pp.125-128, 2013.

K. Cormac-flanagan, M. Rustan, M. Leino, G. Lillibridge, J. B. Nelson et al., Extended static checking for Java, PLDI, pp.234-245, 2002.

C. Flanagan and J. B. Saxe, Avoiding exponential explosion: generating compact verification conditions, POPL, pp.193-205, 2001.

Y. R. Mikhail, F. R. Gadelha, J. Monteiro, L. C. Morse, B. Cordeiro et al., ESBMC 5.0: an industrial-strength C model checker, ASE, pp.888-891, 2018.

P. Herms, C. Marché, and B. Monate, A certified multiprover verification condition generator, VSTTE, vol.7152, pp.2-17, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00639977

D. Hoang, Y. Moy, A. Wallenburg, and R. Chapman, SPARK 2014 and GNATprove -A competition report from builders of an industrial-strength verifying compiler, STTT, vol.17, issue.6, pp.695-707, 2015.

C. A. Hoare, An axiomatic basis for computer programming, Commun. ACM, vol.12, issue.10, pp.576-580, 1969.

T. Kleymann, Hoare logic and auxiliary variables, Formal Asp. Comput, vol.11, issue.5, pp.541-566, 1999.

H. Lehner and P. Müller, Formal translation of bytecode into BoogiePL, Electr. Notes Theor. Comput. Sci, vol.190, issue.1, pp.35-50, 2007.

K. and R. M. Leino, Dafny: An automatic program verifier for functional correctness, LPAR (Dakar), vol.6355, pp.348-370, 2010.

K. , R. M. Leino, J. B. Saxe, and R. Stata, Checking Java programs via guarded commands, ECOOP Workshops, vol.1743, pp.110-111, 1999.

C. Belo-lourenço, M. J. Frade, S. Nakajima, and J. S. Pinto, A generalized approach to verification condition generation, COMPSAC (1), pp.194-203, 2018.

C. Belo-lourenço, M. J. Frade, and J. S. Pinto, Formalizing single-assignment program verification: An adaptationcomplete approach, ESOP, vol.9632, pp.41-67, 2016.

C. Belo and L. , Single-assignment programs verification, 2018.

F. Merz, S. Falke, and C. Sinz, LLBMC: bounded model checking of C and C++ programs using a compiler IR, VSTTE, vol.7152, pp.146-161, 2012.

P. Vanbroekhoven, G. Janssens, M. Bruynooghe, and F. Catthoor, A practical dynamic single assignment transformation, ACM Trans. Design Autom. Electr. Syst, vol.12, issue.4, p.40, 2007.

F. Vogels, B. Jacobs, and F. Piessens, A machine checked soundness proof for an intermediate verification language, SOFSEM, vol.5404, pp.570-581, 2009.