J. , The B-book -assigning programs to meanings, 2005.

J. , Modeling in Event-B -System and Software Engineering, 2010.

H. Barendregt, Introduction to generalized type systems, Journal of Functional Programming, vol.1, issue.2, pp.125-154, 1991.

G. Barthe, P. R. D'argenio, and T. Rezk, Secure information flow by selfcomposition, Mathematical Structures in Computer Science, vol.21, issue.6, pp.1207-1252, 2011.

S. Bechtold, S. Brannen, J. Link, M. Merdes, M. Philipp et al., JUnit 5 User Guide

A. Blanchard, N. Kosmatov, and F. Loulergue, Ghosts for lists: A critical module of contiki verified in frama-c, NFM, vol.10811, pp.37-53, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01720401

S. Blazy, D. Bühler, and B. Yakobowski, Structuring abstract interpreters through state and value abstractions, Verification, Model Checking, and Abstract Interpretation -18th International Conference, vol.10145, pp.112-130, 2017.
URL : https://hal.archives-ouvertes.fr/cea-01808886

C. Dubois and V. Ménissier-morain, Apprentissage de la programmation avec OCaml, Hermès Sciences, 2004.
URL : https://hal.archives-ouvertes.fr/hal-01124971

J. Filliâtre and A. Paskevich, Why3 -where programs meet provers, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, vol.7792, pp.125-128, 2013.

N. Huynh, M. Frappier, A. Mammar, R. Laleau, and J. Desharnais, A formal validation of the RBAC ANSI 2012 standard using B, Sci. Comput. Program, vol.131, pp.76-93, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01390991

A. Jarrar and Y. Balouki, Formal modeling of a complex adaptive air traffic control system, CASM, vol.6, issue.6, 2018.

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

N. Kosmatov, N. Williams, B. Botella, and M. Roger, Structural unit testing as a service with pathcrawler-online.com, SOSE, pp.435-440, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01810293

T. Lecomte, D. Déharbe, É. Prun, and E. Mottin, Applying a formal method in industry: A 25-year trajectory, Formal Methods: Foundations and Applications -20th Brazilian Symposium, vol.10623, pp.70-87, 2017.

A. Miné, A new numerical abstract domain based on difference-bound matrices. CoRR, abs/cs/0703073, 2007.

D. Monniaux and L. Gonnord, Cell morphing: From array programs to array-free horn clauses, SAS, vol.9837, pp.361-382, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01206882

B. C. Pierce, Types and programming languages, 2002.

G. Ro?u and T. F. ?erb?nu??, An overview of the K semantic framework, Journal of Logic and Algebraic Programming, vol.79, issue.6, pp.397-434, 2010.

I. Vistbakka and E. Troubitsyna, Towards Integrated Modelling of Dynamic Access Control with UML and Event-B. arXiv e-prints, 2018.