1997-2021 Publications
All
Articles
Book chapters
Communications
Posters
Thesis
Other 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 28th 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
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 - 14th 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 10th 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 1st 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, 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 ”, 1st 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 24th 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
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 - 4th 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 - 12th 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 ”, 23th 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 ”, 4e 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
1998
1997