P. Baudin, P. Cuoq, J. C. Filliâtre, C. Marché, B. Monate et al., ACSL: ANSI/ISO C Specification Language

A. Blanchard, N. Kosmatov, and F. Loulergue, Ghosts for Lists: A Critical Module of??Contiki Verified in Frama-C, Proc. of the 10th NASA Formal Methods Symposium (NFM 2018), pp.37-53, 2018.
DOI : 10.1145/3133956.3133974
URL : https://hal.archives-ouvertes.fr/hal-01720401

´. A. Darvas and P. Müller, Proving Consistency and Completeness of Model Classes Using Theory Interpretation, Proc. of the 13th International Conference on Fundamental Approaches to Software Engineering, pp.218-232, 2010.
DOI : 10.1007/978-3-642-12029-9_16
URL : https://link.springer.com/content/pdf/10.1007%2F978-3-642-12029-9_16.pdf

M. Delahaye, N. Kosmatov, and J. Signoles, Common specification language for static and dynamic analysis of C programs, Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC '13, pp.1230-1235, 2013.
DOI : 10.1145/2480362.2480593
URL : https://hal.archives-ouvertes.fr/hal-00853721

A. Dunkels, B. Grönvall, and T. Voigt, Contiki - a lightweight and flexible operating system for tiny networked sensors, 29th Annual IEEE International Conference on Local Computer Networks, pp.455-462, 2004.
DOI : 10.1109/LCN.2004.38
URL : http://www.sics.se/~adam/dunkels04contiki.pdf

C. Gladisch and S. S. Tyszberowicz, Specifying linked data structures in JML for combining formal verification and testing, Science of Computer Programming, vol.107, issue.108, pp.107-108, 2015.
DOI : 10.1016/j.scico.2015.02.005

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
URL : https://hal.archives-ouvertes.fr/cea-01808981

C. Kolias, G. Kambourakis, A. Stavrou, and J. M. Voas, DDoS in the IoT: Mirai and Other Botnets, Computer, vol.50, issue.7, pp.80-84, 2017.
DOI : 10.1109/MC.2017.201

G. C. Necula, S. Mcpeak, S. P. Rahul, and W. Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proc. of the 11th International Conference on Compiler Construction, pp.213-228, 2002.
DOI : 10.1007/3-540-45937-5_16
URL : https://link.springer.com/content/pdf/10.1007%2F3-540-45937-5_16.pdf

N. Polikarpova, C. A. Furia, and B. Meyer, Specifying Reusable Components, Proc. of the 3rd International Conference on Verified Software: Theories, Tools, Experiments, pp.127-141, 2010.
DOI : 10.1007/978-3-642-15057-9_9
URL : http://se.inf.ethz.ch/people/furia/pubs/SpecifyingReusableComponents-TR10.pdf

J. Signoles, E-ACSL: Executable ANSI/ISO C Specification Language

, The Coq Development Team: The Coq proof assistant

P. Tollitte, D. Delahaye, and C. Dubois, Producing Certified Functional Code from Inductive Specifications, Proc. of the 2nd International Conference on Certified Programs and Proofs, pp.76-91, 2012.
DOI : 10.1007/978-3-642-35308-6_9
URL : https://hal.archives-ouvertes.fr/hal-01126212

K. Vorobyov, J. Signoles, and N. Kosmatov, Shadow state encoding for efficient monitoring of block-level properties, Proc. of the International Symposium on Memory Management, pp.47-58, 2017.
URL : https://hal.archives-ouvertes.fr/cea-01836510