Postdoc at University Paris-Sud (December 2019 ->)
I work on formal verification for quantum programs, in the group of Benoît Valiron. More precisely, I develop a core programming languages, called qbricks, that enables the writing of entirely certified quantum scale invariant quantum programs. Qbricks is embedded in the language WhyML, (cosine o) ( sine o)an ML-like language that is designed for formal verification of annotated functional programs. Thanks to the verification and interactive proof tool Why3, a WhyML program generates proof obligations that are formatted for different SMT solver and proof assistants. Proofs for qbricks programs are rooted in both matrix and path-sum semantics.
Research Engineer (CDD) in CEA List (April 2018 -> October 2019)
Iniating, the work I am now leading in University Paris Sud, I started developing Qbricks. My work in CEA enabled me to implement, specify, verify, present in several seminars and workshops and submit for PLDI, the first ever communicated example of a non-trivial parametric formally verified quantum algorithm (phase estimation algorithm).
Postdoc in LORIA (Nancy), Cello group (September 2016 -> December 2017)
I integrated Cello group in september 2016. There, I worked on strategic epistemic logics. Especially, I developped a language called Past Knowledge Epistemic Logic (PKSL). This language provides tools to characterize, in a semantic game, the knowledge agents may or may not have about the strategic context and the knowledge they may or may not have about the past. This expressivity, combined with the characterization of knowledge about the future, enables more structure time sequenced assertions, like couterfactuals statements and the ability of agents to observe them. I also developped, as a case for PKSL, a modelling for the quantum cryptographic protocol BB84.
Postdoc in Ecole Polytechnique de Montréal, CRAC group, Project VerITTAS (Verification and Integration of multi-critical Time Triggered Avionics Systems) (AVIO613) March -> December 2015.
Project VerITTAS aimed at applying Model Driven Architectures to build Time Triggered Architectures (TTA), defining models and automatic techniques for developing and integrating TTA based mixed criticality avionic systems, and experimenting integrated modular avionics (IMA) systems using TTA based data communication networks. I developped a modeling language for systems based on an IMA architectures whose modules are interconnected via a TT-EThernet network. I also developed a tool based on NuSMV and enabling simulations for such a systems and computations and checking of various performance properties(report).
PhD Thesis
I defended my PhD thesis on June 20th 2014.(Abstract in french) (Abstract in english) (Slides) (Manuscript)(Diploma)(Defense report).