A survey of symbolic execution techniques, ACM Comput. Surv, vol.51, issue.3, 2018. ,
Boogie: A modular reusable verifier for object-oriented programs, FMCO, vol.4111, pp.364-387, 2005. ,
Specification and verification: the Spec# experience, Commun. ACM, vol.54, issue.6, pp.81-91, 2011. ,
Bounded model checking, Advances in Computers, vol.58, pp.117-148, 2003. ,
A reachability predicate for analyzing low-level software, TACAS, vol.4424, pp.19-33, 2007. ,
A tool for checking ANSI-C programs, TACAS, vol.2988, pp.168-176, 2004. ,
Soundness and completeness of an axiom system for program verification, SIAM J. Comput, vol.7, issue.1, pp.70-90, 1978. ,
Efficiently computing static single assignment form and the control dependence graph, ACM Trans. Program. Lang. Syst, vol.13, issue.4, pp.451-490, 1991. ,
Effectively eliminating auxiliaries, Theory and Practice of Formal Methods, vol.9660, pp.226-241, 2016. ,
Extended static checking, Research report, vol.159, 1998. ,
A Discipline of Programming, 1976. ,
Why3 -where programs meet provers, ESOP, vol.7792, pp.125-128, 2013. ,
Extended static checking for Java, PLDI, pp.234-245, 2002. ,
Avoiding exponential explosion: generating compact verification conditions, POPL, pp.193-205, 2001. ,
ESBMC 5.0: an industrial-strength C model checker, ASE, pp.888-891, 2018. ,
A certified multiprover verification condition generator, VSTTE, vol.7152, pp.2-17, 2012. ,
URL : https://hal.archives-ouvertes.fr/hal-00639977
SPARK 2014 and GNATprove -A competition report from builders of an industrial-strength verifying compiler, STTT, vol.17, issue.6, pp.695-707, 2015. ,
An axiomatic basis for computer programming, Commun. ACM, vol.12, issue.10, pp.576-580, 1969. ,
Hoare logic and auxiliary variables, Formal Asp. Comput, vol.11, issue.5, pp.541-566, 1999. ,
Formal translation of bytecode into BoogiePL, Electr. Notes Theor. Comput. Sci, vol.190, issue.1, pp.35-50, 2007. ,
Dafny: An automatic program verifier for functional correctness, LPAR (Dakar), vol.6355, pp.348-370, 2010. ,
Checking Java programs via guarded commands, ECOOP Workshops, vol.1743, pp.110-111, 1999. ,
A generalized approach to verification condition generation, COMPSAC (1), pp.194-203, 2018. ,
Formalizing single-assignment program verification: An adaptationcomplete approach, ESOP, vol.9632, pp.41-67, 2016. ,
Single-assignment programs verification, 2018. ,
LLBMC: bounded model checking of C and C++ programs using a compiler IR, VSTTE, vol.7152, pp.146-161, 2012. ,
A practical dynamic single assignment transformation, ACM Trans. Design Autom. Electr. Syst, vol.12, issue.4, p.40, 2007. ,
A machine checked soundness proof for an intermediate verification language, SOFSEM, vol.5404, pp.570-581, 2009. ,