E. Alkassar, E. Cohen, M. Kovalev, and W. J. Paul, Verification of TLB Virtualization Implemented in C, Proc. of the 4th International Conference on Verified Software: Theories, Tools, Experiments, pp.209-224, 2012.
DOI : 10.1145/1629575.1629596

E. Alkassar, W. Paul, A. Starostin, and A. Tsyban, Pervasive Verification of an OS Microkernel, Proc. of the 3rd International Conference on Verified Software: Theories, Tools, Experiments, pp.71-85, 2010.
DOI : 10.1007/978-3-642-15057-9_5

G. Barthe, G. Betarte, J. D. Campo, J. M. Chimento, and C. Luna, Formally verified implementation of an idealized model of virtualization

P. Baudin, P. Cuoq, J. Fillitre, C. March, B. Monate et al., ACSL: ANSI/ISO C Specification Language

E. Biham and A. Shamir, Differential Cryptanalysis of the Data Encryption Standard, 1993.
DOI : 10.1007/978-1-4613-9314-6

A. Blanchard, N. Kosmatov, M. Lemerre, and F. Loulergue, A Case Study on Formal Verification of the Anaxagoros Hypervisor Paging System with Frama-C, Proc. of the 20th International Workshop on Formal Methods for Industrial Critical Systems, pp.15-30, 2015.
DOI : 10.1007/978-3-319-19458-5_2

S. Conchon, The Alt-Ergo Automated Theorem Prover

J. Daemen and V. Rijmen, The Design of Rijndael: AES -The Advanced Encryption Standard. Information Security and Cryptography, 2002.
DOI : 10.1007/978-3-662-04722-4

L. De-moura and N. Bjørner, Z3: An Efficient SMT Solver, Proc. of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.337-340, 2008.
DOI : 10.1007/978-3-540-78800-3_24

A. Dunkels, B. Gronvall, and T. Voigt, Contiki - a lightweight and flexible operating system for tiny networked sensors, 29th Annual IEEE International Conference on Local Computer Networks, 2004.
DOI : 10.1109/LCN.2004.38

F. Kirchner, N. Kosmatov, V. Prevosto, J. Signoles, and B. Yakobowski, Frama-C: A software analysis perspective. Formal Asp, Comput, vol.27, issue.3, pp.573-609, 2015.
DOI : 10.1007/s00165-014-0326-7

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4, Communications of the ACM, vol.53, issue.6, pp.107-115, 2010.
DOI : 10.1145/1743546.1743574

F. Mangano, S. Duquennoy, and N. Kosmatov, A memory allocation module of Contiki formally verified with Frama-C. A case study, Proc. of the 11th International Conference on Risks and Security of Internet and Systems, pp.114-120, 2016.

S. Raza, S. Duquennoy, J. Höglund, U. Roedig, and T. Voigt, Secure communication for the Internet of Things-a comparison of link-layer security and IPsec for 6LoWPAN, Security and Communication Networks, vol.19, issue.2, pp.72654-2668, 2014.
DOI : 10.1108/10662240910952373

S. Raza, T. Helgason, P. Papadimitratos, and T. Voigt, SecureSense: End-to-end secure communication architecture for the cloud-connected Internet of Things, Future Generation Computer Systems, vol.77, pp.40-51, 2017.
DOI : 10.1016/j.future.2017.06.008

S. Raza, L. Seitz, D. Sitenkov, and G. Selander, S3K: Scalable Security With Symmetric Keys???DTLS Key Establishment for the Internet of Things, IEEE Transactions on Automation Science and Engineering, vol.13, issue.3, pp.1270-1280, 2016.
DOI : 10.1109/TASE.2015.2511301

V. Van-der-veen, N. Dutt-sharma, L. Cavallaro, and H. Bos, Memory Errors: The Past, the Present, and the Future, Proc. of the International Symposium on Research in Attacks, Intrusions, and Defenses, pp.86-106, 2012.
DOI : 10.1007/978-3-642-33338-5_5