The B-Book, Assigning Programs to Meanings ,
Formal Validation of Model transformation with Coq Proof Assistant, New Technologies of Information and Communication (NTIC), pp.1-6, 2015. ,
A Formally Verified Compiler for Lustre, Programming Language Design and Implementation (PLDI), pp.586-601, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01512286
A Type-Theoretic Framework for Certified Model Transformations, Brazilian Symposium on Formal Methods (SBMF), vol.6527, pp.112-127, 2010. ,
Experimenting Formal Proofs of Petri Nets Refinements, Electronic Notes in Theoretical Computer Science (ENTCS), vol.214, pp.231-254, 2008. ,
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
Formal Semantics for VHDL, 1995. ,
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
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
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
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. ,
Introduction to the Coq Proof-Assistant for Practical Software Verification, LASER Summer School on Software Engineering, vol.7682, pp.45-95, 2011. ,
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.
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