Two PhD students at Sorbonne University (Supervision / Co-supervision)

Eight past PhD students (2006 - 2023) at Sorbonne University

Two past Postdoc (1996 - 2015) at Sorbonne University

1997-2021 Publications

• 2021
  • N. Belleville, D. Couroussé, E. Encrenaz, K. Heydemann, Q. Meunier : “PROSECCO: Formally-proven secure compiled code”, Automation in Cybersecurity 2021 - Proceedings of the 28^th Computer & Electronics Security Application Rendezvous (C&ESAR 2021), vol. 3056, CEUR Workshop Proceedings, Rennes, France, pp. 13-25, (ceur-ws.org) (2021)
• 2019
  • I. Ben El Ouahma, Q. Meunier, K. Heydemann, E. Encrenaz : “Side-channel robustness analysis of masked assembly codes using a symbolic approach”, Journal of Cryptographic Engineering, pp. 1-12, (Springer) (2019)
  • J.‑B. Bréjon, K. Heydemann, E. Encrenaz, Quentin L. Meunier, S. Vu : “Fault attack vulnerability assessment of binary code”, Cryptography and Security in Computing Systems (CS2’19), Valencia, Spain, pp. 13-18, (ACM) (2019)
• 2018
  • Quentin L. Meunier, Y. Thierry Mieg, E. Encrenaz : “Modeling a Cache Coherence Protocol with the Guarded Action Language”, Workshop on Models for Formal Analysis of Real Systems, Thessaloniki, Greece (2018)
• 2017
  • I. Ben El Ouahma, Quentin L. Meunier, K. Heydemann, E. Encrenaz : “Symbolic Approach for Side-Channel Resistance Analysis of Masked Assembly Codes”, Security Proofs for Embedded Systems, Taipei, China (2017)
• 2016
  • L. Goubet, K. Heydemann, E. Encrenaz, R. De Keulenaer : “Efficient Design and Evaluation of Countermeasures against Fault Attack with Formal Verification”, Smart Card Research and Advanced Applications - 14^th International Conference, CARDIS 2015, Bochum, Germany, November 4-6, 2015. Revised Selected Paper, vol. 9514, Lecture Notes in Computer Science, Bochum, Germany, pp. 177-192, (Springer International Publishing) (2016)
• 2015
  • H. Mokrani, R. Ameur‑Boulifa, E. Encrenaz : “Assisting Refinement in System-on-Chip Design”, chapter in Languages, Design Methods, and Tools for Electronic System Design, Selected Contributions from FDL 2013, vol. 311, Lecture Notes in Electrical Engineering, pp. 21-42, (Springer) (2015)
• 2014
  • S.‑H. Syed‑Alwi, E. Encrenaz : “FSM-based properties and abstraction of components”, IEEE International Symposium on Rapid System Prototyping, New Delhi, India, pp. 37-43, (IEEE) (2014)
  • N. Moro, K. Heydemann, E. Encrenaz, B. Robisson : “Formal verification of a software countermeasure against instruction skip attacks”, Journal of Cryptographic Engineering, vol. 4 (3), pp. 145-156, (Springer) (2014)
  • N. Moro, K. Heydemann, A. Dehbaoui, B. Robisson, E. Encrenaz : “Fault attacks on two software countermeasures”, TRUDEVICE 2014, Paderborn, Germany (2014)
  • N. Moro, K. Heydemann, A. Dehbaoui, B. Robisson, E. Encrenaz : “Experimental evaluation of two software countermeasures against fault attacks”, 2014 IEEE International Symposium on Hardware-Oriented Security and Trust (HOST), Arlington, United States, pp. 112-117 (2014)
• 2013
  • N. Moro, A. Dehbaoui, K. Heydemann, B. Robisson, E. Encrenaz : “Electromagnetic fault injection on microcontrollers”, Chip-to-Cloud Security Forum 2013, Nice, France (2013)
  • H. Mokrani, R. Ameur‑Boulifa, E. Encrenaz : “Assisting Refinement in System on Chip Design”, Forum on Specification and Design Languages, Paris, France, pp. 1-6, (IEEE) (2013)
  • K. Heydemann, N. Moro, E. Encrenaz, B. Robisson : “Formal verification of a software countermeasure against instruction skip attacks”, PROOFS 2013, Santa-Barbara, United States (2013)
  • N. Moro, A. Dehbaoui, K. Heydemann, B. Robisson, E. Encrenaz : “Electromagnetic fault injection: towards a fault model on a 32-bit microcontroller”, Proceedings of the 10^th workshop on Fault Diagnosis and Tolerance in Cryptography, Santa-Barbara, United States, pp. 77-88 (2013)
  • G. Plouviez, E. Encrenaz, F. Wajsbürt : “A formally verified hypervisor with hardware support for a many-core chip”, The 1^st Workshop on Runtime and Operating Systems for the Many-core Era, ROME 2013, vol. 8374, Lecture Notes in Computer Science, Aachen, Germany, pp. 801-811, (Springer) (2013)
  • S.‑H. Syed‑Alwi, C. Braunstein, E. Encrenaz : “Efficient Refinement Strategy Exploiting Component Properties in a CEGAR Process”, chapter in Models, Methods and Tools for Complex Chip Design, selected contributions from FDL 2012, vol. 265, Lecture Notes in Electrical Engineering, pp. 17-36, (Springer) (2013)
• 2012
  • S.‑H. Syed‑Alwi, C. Braunstein, E. Encrenaz : “AN EFFICIENT REFINEMENT STRATEGY EXPLOITING COMPONENT PROPERTIES IN A CEGAR PROCESS”, Forum on specification & Design Languages (FDL 2012), Vienne, Austria, pp. 27-34 (2012)
  • H. Le Bouder, N. Moro, B. Robisson, E. Encrenaz, A. Tria : “Un formalisme commun aux attaques par canaux auxiliaires et par injection de fautes”, Colloque National GDR SOC-SIP 2012, Paris, France (2012)
• 2011
  • H. Mokrani, R. Ameur‑Boulifa, E. Encrenaz, S. Coudert : “Approche pour l’intégration du raffinement formel dans le processus de conception des SOC”, Journal Européen des Systèmes Automatisés (JESA), vol. 45 (1-3), pp. 221-236, (Lavoisier) (2011)
  • S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, I. Mounier, D. Poitrenaud, S. Younes : “Feasibility Analysis for Robustness Quantification by Symbolic Model Checking”, Formal Methods in System Design, vol. 39 (2), pp. 165-184, (Springer Verlag) (2011)
• 2010
  • A. Bara, P. Bazargan Sabet, R. Chevallier, E. Encrenaz, D. Le Dû, P. Renault : “Formal Verification of Timed VHDL Programs”, Forum on Specification & Design Languages, FDL 2010, Southampton, United Kingdom, pp. 80-85, (IET) (2010)
  • V. Beaudenon, E. Encrenaz, S. Taktak : “Data Decision Diagrams for Promela Systems Analysis”, International Journal on Software Tools for Technology Transfer, vol. 12 (5), pp. 337-352, (Springer Verlag) (2010)
  • S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, T. Li, I. Mounier, D. Poitrenaud, S. Younes : “Quantifying Robustness by Symbolic Model checking”, 1^st Hardware Verification Workshop (CAV workshop), Edinburgh, United Kingdom, pp. 1-12 (2010)
  • S. Taktak, E. Encrenaz, J.‑L. Desbarbieux : “A polynomial algorithm to prove deadlock-freeness of wormhole networks”, PDP EUROMICRO Conference on Parallel, Distributed and Network-based Computing IEEE Computer Society, Pisa, Italy, pp. 121-128, (IEEE) (2010)
• 2009
  • É. André, E. Encrenaz, L. Fribourg, Th. Chatain : “An Inverse Method for Parametric Timed Automata”, International Journal of Foundations of Computer Science, vol. 20 (5), pp. 819-836, (World Scientific Publishing) (2009)
  • E. Encrenaz, A. Finkel : “Automatic Verification of Counter Systems With Ranking Function”, Electronic Notes in Theoretical Computer Science, vol. 239, pp. 85-103, (Elsevier) (2009)
  • R. Chevallier, E. Encrenaz, L. Fribourg, W. Xu : “Timed Verification of the Generic Architecture of a Memory Circuit Using Parametric Timed Automata”, Formal Methods in System Design, vol. 34 (1), pp. 59-81, (Springer Verlag) (2009)
  • S. Baarir, C. Braunstein, R. Clavel, E. Encrenaz, J.‑M. Ilié, R. Leveugle, I. Mounier, L. Pierre, D. Poitrenaud : “Complementary formal approaches for dependability analysis”, The 24^th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, Chicago, Illinois, United States, pp. 331-339, (IEEE Computer Society) (2009)
• 2008
  • É. André, Th. Chatain, E. Encrenaz, L. Fribourg : “An Inverse Method for Parametric Timed Automata”, Proceedings of the Second Workshop on Reachability Problems in Computational Models (RP 2008), vol. 223, Electronic Notes in Theoretical Computer Science, Liverpool, United Kingdom, pp. 29-46, (Elsevier) (2008)
  • S. Taktak, J.‑L. Desbarbieux, E. Encrenaz : “A tool for automatic detection of deadlocks in wormhole networks on chip”, ACM Transactions on Design Automation of Electronic Systems, vol. 13 (1), pp. 1-8, (Association for Computing Machinery) (2008)
• 2007
  • E. Encrenaz : “Contributions pour la conception et la vérification de systèmes matériels embarqués”, habilitation, phd defence 06/18/2007 (2007)
  • C. Braunstein, E. Encrenaz : “Using CTL formulae as component abstraction in a design and verification flow”, ACSD IEEE International Conference on Application of Concurrency to System Design, Bratislava, Slovakia, pp. 80-89, (IEEE) (2007)
  • C. Braunstein, E. Encrenaz : “CTL-property Transformations along an Incremental Design Process”, International Journal on Software Tools for Technology Transfer, vol. 9 (1), pp. 77-88, (Springer Verlag) (2007)
  • E. Encrenaz, A. Finkel : “Automatic Verification of Counter Systems with Ranking Functions”, INFINITY International Symposium on Infinite-Space Systems, Porto, Portugal (2007)
• 2006
  • C. Braunstein, E. Encrenaz : “A Further Step in the Incremental Design Process: Incorporation of an Increment Specification”, LPAR IEEE International Conference on Logic for Programming Artificial Intelligence and Reasoning, Phnom Penh, Cambodia, pp. short paper (2006)
  • S. Taktak, E. Encrenaz, J.‑L. Desbarbieux : “A Tool for Automatic Detection of Deadlock in Wormhole Networks on Chip”, HLDVT IEEE International High Level Design Validation and Test Workshop, Monterey, California, United States, pp. 203-210, (IEEE) (2006)
  • E. Encrenaz, L. Fribourg : “Time separation of events, an inverse method”, LIX Colloquium on emerging Trends in Concurrency Theory, Palaiseau, France (2006)
  • C. Braunstein, E. Encrenaz : “Formalizing the incremental design and verification process of a pipelined protocol converter”, RSP International Workshop on Rapid System Prototyping, Chania, Crete, Greece, pp. 103-109, (IEEE) (2006)
• 2005
  • V. Beaudenon, E. Encrenaz, S. Taktak : “Data Decision Diagrams for ProMeLa Systems Analysis”, (2005)
  • C. Braunstein, E. Encrenaz : “CTL-property transformations along an incremental design process”, (2005)
• 2004
  • V. Beaudenon, E. Encrenaz : “Utilisation de Diagrammes de Décision de Données pour la Vérification Fonctionnelle de Systèmes Matériels”, MAJECTSTIC 2004 - MAnifestation des JEunes Chercheurs STIC, Calais, France (2004)
  • C. Braunstein, E. Encrenaz : “CTL-Property Transformations along an Incremental Design Process”, AVOCS 2004 - 4^th International Workshop on Automated Verification of Critical Systems, London, United Kingdom, pp. 263-278 (2004)
  • H. Charlery, A. Greiner, E. Encrenaz, L. Mortiez, A. Andriahantenaina : “Using VCI in a on-chip system around SPIN network”, MIXDES Mixed Design of Integrated Circuits and Systems, Szczecin, Poland, pp. 571-576 (2004)
• 2003
  • C. Roux, E. Encrenaz : “CTL May Be Ambiguous When Model Checking Moore Machines”, CHARME 2003 - 12^th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, vol. 2860, Lecture Notes in Computer Science, L'Aquila, Italy, pp. 164-169, (Springer) (2003)
  • H. Charlery, E. Encrenaz, A. Greiner, A. Andriahantenaina, L. Mortiez : “SPIN, un micro-réseau d’interconnexion à commutation de paquets respectant la norme VCI. Concepts généraux et validation.”, Symposium en Architecture et Adequation Algorithme Architecture (SympAAA 2003), La Colle sur Loup, France, pp. 337-344 (2003)
  • V. Beaudenon, E. Encrenaz, J.‑L. Desbarbieux : “Design Validation of ZCSP with SPIN”, IEEE Third International Conference on Application of Concurrency to System Design (ACSD 2003), Guimaraes, Portugal, pp. 102-110, (IEEE) (2003)
  • V. Beaudenon, E. Encrenaz, J.‑L. Desbarbieux : “Design Validation of ZCSP with SPIN”, (2003)
• 2002
  • J.‑M. Couvreur, E. Encrenaz, E. Paviot‑Adet, D. Poitrenaud, P.‑A. Wacrenier : “Data Decision Diagrams for Petri Net analysis”, 23^th International Conference on Application and Theory of Petri Nets, vol. 2360, Lecture Notes in Computer Science, Adelaide, Australia, pp. 101-120, (Springer-Verlag) (2002)
  • E. Encrenaz, A. Munier, F. Pétrot : “Minimisation de la taille des buffers entre tâches communicantes pour la conception de composants embarqués”, 4^e Congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision (ROADEF 2002), Paris, France, pp. 230 (2002)
• 2000
  • G. Decuq, E. Encrenaz : “Extension des diagrammes de décisions binaires pour la représentation de programmes VHDL en vue de leur vérification”, (2000)
• 1998
  • F. Rahim, E. Encrenaz, M. Minoux, Rajesh K. Bawa : “Modular Model Checking of VLSI Designs described in VHDL”, IEEE International Conference on Computer and their Applications, Honolulu, Hawai, United States, pp. 365-368 (1998)
• 1997
  • F. Rahim, E. Encrenaz : “Property-dependant bisimulation for compositional model-checking”, (1997)