3 Doctorants (Direction de recherche / Co-encadrement)

• BEN EL OUAHMA Ines : Modélisation de la robustesse d'un code assembleur contre les attaques par observation.
• BREJON Jean-Baptiste : Quantification de la sécurité des applications en présence d’attaques physiques et détection de chemins d’attaques .
• EZVAN Bruno : Environnement pour la certification de composants matériels et logiciels.

5 Docteurs 2006 - 2014

Publications 1998-2017

• 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)
• 2015
  • L. Goubet, K. Heydemann, E. Encrenaz, R. De Keulenaer : “Efficient Design and Evaluation of Countermeasures against Fault Attack with Formal Verification”, 14^th International conference Smart Card Research and Advanced Applications (CARDIS), vol. 9514, Lecture Notes in Computer Science, Bochum, Germany, pp. 177-192, (Springer) (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, T. Maehne, M.-M. Louërat (Eds.), pp. 21-42, (Springer), (ISBN: 978-3-319-06317-1) (2015)
• 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), H. Springer Berlin (Ed.), pp. 145-156, (ISBN: 2190-8508) (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, USA, pp. 112-117, (IEEE) (2014)
  • N. Moro, K. Heydemann, A. Dehbaoui, B. Robisson, E. Encrenaz : “Fault attacks on two software countermeasures”, TRUDEVICE 2014, Paderborn, Germany (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)
• 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)
  • 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)
  • N. Moro, A. Dehbaoui, K. Heydemann, B. Robisson, E. Encrenaz : “Electromagnetic fault injection on microcontrollers”, Chip-to-Cloud Security Forum 2013, Nice, France (2013)
  • N. Moro, A. Dehbaoui, K. Heydemann, B. Robisson, E. Encrenaz : “Electromagnetic Fault Injection: towards a Fault Model on a 32-bit Microcontroller”, 10^th workshop on Fault Diagnosis and Tolerance in Cryptography - FDTC 2013, Santa-Barbara, USA, pp. 77-88, (IEEE) (2013)
  • K. Heydemann, N. Moro, E. Encrenaz, B. Robisson : “Formal verification of a software countermeasure against instruction skip attacks”, PROOFS 2013, Santa-Barbara, USA (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), (ISBN: 978-3-319-01417-3) (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, (IEEE) (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, (ISBN: 1269-6935) (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, (ISBN: 0925-9856) (2011)
• 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, (ISBN: 1433-2779) (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)
  • 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)
  • 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)
• 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, (ISBN: 0129-0541) (2009)
  • E. Encrenaz, A. Finkel : “Automatic Verification of Counter Systems With Ranking Function”, Electronic Notes in Theoretical Computer Science, vol. 239, pp. 85-103, (ISBN: 1571-0661) (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, (ISBN: 0925-9856) (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, USA, pp. 331-339, (IEEE Computer Society) (2009)
• 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, (ISBN: 1084-4309) (2008)
  • E. Encrenaz, L. Fribourg : “Time Separation of Events: an Inverse Method”, Electronic Notes in Theoretical Computer Science, vol. 209, pp. 135-148, (ISBN: 1571-0661) (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)
• 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, (ISBN: 1433-2779) (2007)
  • E. Encrenaz, A. Finkel : “Automatic Verification of Counter Systems with Ranking Functions”, INFINITY International Symposium on Infinite-Space Systems, Porto, Portugal (2007)
  • C. Braunstein, E. Encrenaz : “Using CTL formulae as component abstraction in a design and verification flow”, Application of Concurrency to System Design ACSD IEEE International Conference on Application of Concurrency to System Design, Bratislava, Slovakia, pp. 80-89, (IEEE) (2007)
  • E. Encrenaz : “Contributions pour la conception et la vérification de systèmes matériels embarqués”, habilitation à diriger des recherches, soutenance 18/06/2007 (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, USA, pp. 203-210, (IEEE) (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)
  • E. Encrenaz, L. Fribourg : “Time separation of events, an inverse method”, LIX Colloquium on emerging Trends in Concurrency Theory, Palaiseau, France (2006)
• 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)
  • 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)
• 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)
  • 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)
  • 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)
• 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, J. Esparza Lakos (Ed.), 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ème 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)
• 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, USA, pp. 365-368 (1998)