J. , The B-Book, Assigning Programs to Meanings

K. Berramla, E. A. Deba, and M. Senouci, Formal Validation of Model transformation with Coq Proof Assistant, New Technologies of Information and Communication (NTIC), pp.1-6, 2015.

T. Bourke, L. Brun, P. Dagand, X. Leroy, M. Pouzet et al., A Formally Verified Compiler for Lustre, Programming Language Design and Implementation (PLDI), pp.586-601, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01512286

D. Calegari, C. Luna, N. Szasz, and A. Tasistro, A Type-Theoretic Framework for Certified Model Transformations, Brazilian Symposium on Formal Methods (SBMF), vol.6527, pp.112-127, 2010.

C. Choppy, M. Mayero, and L. Petrucci, Experimenting Formal Proofs of Petri Nets Refinements, Electronic Notes in Theoretical Computer Science (ENTCS), vol.214, pp.231-254, 2008.

L. Fronc and F. Pommereau, Towards a Certified Petri Net Model-Checker, Asian Symposium on Programming Languages and Systems (APLAS), vol.7078, pp.322-336, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00666660

C. D. Kloos and P. Breuer, Formal Semantics for VHDL, 1995.

H. Leroux, Handling Exceptions in Petri Net-Based Digital Architecture: From Formalism to Implementation on FPGAs, IEEE Transactions Industrial Informatics, vol.11, issue.4, pp.897-906, 2015.
URL : https://hal.archives-ouvertes.fr/lirmm-01241168

H. Leroux, K. Godary-dejean, and D. Andreu, Complex Digital System Design: A Methodology and Its Application to Medical Implants, Formal Methods for Industrial Critical Systems (FMICS), pp.94-107, 2013.
URL : https://hal.archives-ouvertes.fr/lirmm-01064165

X. Leroy, Formal Verification of a Realistic Compiler, Communications of the ACM (CACM), vol.52, issue.7, pp.107-115, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00415861

S. Meghzili, A. Chaoui, M. Strecker, and E. Kerkouche, On the Verification of UML State Machine Diagrams to Colored Petri Nets Transformation Using Isabelle/HOL, Information Reuse and Integration (IRI), pp.419-426, 2017.

C. Paulin-mohring, Introduction to the Coq Proof-Assistant for Practical Software Verification, LASER Summer School on Software Engineering, vol.7682, pp.45-95, 2011.

Y. K. Tan, M. O. Myreen, R. Kumar, A. C. Fox, S. Owens et al., A New Verified Compiler Backend for CakeML, International Conference on Functional Programming (ICFP), pp.60-73, 2016.

, The Coq Development Team. Coq, version 8.11.0. Inria, 2020.

, The IEEE Organization. IEEE Standard VHDL Language Reference Manual -Redline, Revision of IEEE Std 1076-2002) -Redline, pp.1-620, 2009.

Z. Yang, K. Hu, D. Ma, J. Bodeveix, L. Pi et al., From AADL to Timed Abstract State Machines: A Verified Model Transformation, Journal of Systems and Software (JSS), vol.93, pp.42-68, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01123837