K. R. Leino, Dafny: An Automatic Program Verifier for Functional Correctness, LPAR-16, pp.348-370, 2010.
DOI : 10.1007/978-3-642-17511-4_20
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.9592

E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal et al., VCC: A Practical System for Verifying Concurrent C, Theorem Proving in Higher Order Logics (TPHOLs, 2009.
DOI : 10.1007/978-3-540-74591-4_15

B. Jacobs and F. Piessens, The VeriFast program verifier CW Reports CW520, 2008.

J. C. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen, The essence of compiling with continuations, ACM SIGPLAN Notices, vol.28, issue.6, pp.237-247, 1993.
DOI : 10.1145/173262.155113

A. K. Wright and M. Felleisen, A Syntactic Approach to Type Soundness, Information and Computation, vol.115, issue.1, pp.38-94, 1992.
DOI : 10.1006/inco.1994.1093

B. C. Pierce, Types and Programming Languages, 2002.

J. C. Reynolds, The craft of programming. Prentice Hall International series in computer science, 1981.

P. Lucas, Two constructive realizations of the block concept and their equivalence, 1968.

T. Kleymann, Hoare logic and auxiliary variables. Formal Asp, Comput, vol.11, issue.5, pp.541-566, 1999.
DOI : 10.1007/s001650050057
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.27.9009

Z. Zhang, X. Feng, M. Fu, Z. Shao, and Y. Li, A Structural Approach to Prophecy Variables, 9th annual conference on Theory and Applications of Models of Computation (TAMC, pp.61-71, 2012.
DOI : 10.1007/978-3-642-29952-0_12

S. Schmaltz, Towards the Pervasive Formal Verification of Multi-Core Operating Systems and Hypervisors Implemented in C, 2013.

K. R. Leino and M. Moskal, Co-induction Simply, FM 2014: Formal Methods, pp.382-398, 2014.
DOI : 10.1007/978-3-319-06410-9_27

D. E. Denning and P. J. Denning, Certification of programs for secure information flow, Communications of the ACM, vol.20, issue.7, pp.504-513, 1977.
DOI : 10.1145/359636.359712

F. Pottier and S. Conchon, Information flow inference for free, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP'00), pp.46-57, 2000.

F. Pottier and V. Simonet, Information flow inference for ML, ACM Transactions on Programming Languages and Systems, vol.25, issue.1, pp.117-158, 2003.
DOI : 10.1145/596980.596983