About
Yohan BOICHUT is an Assistant Professor at the University of Orleans, Faculty of Science, Department of Computer Science. He is a member of the LMV research team at LIFO (Laboratoire d'Informatique Fondamentale d'Orléans), where he leads significant research in formal methods and security protocol verification. His teaching portfolio spans multiple degree levels including Algorithms and Programming (License 1), Data Bases (License 3 MIAGE), and advanced topics like Security and Specification and Verification at the Master level.
Dr. BOICHUT's research focuses on formal verification techniques, particularly term rewriting systems and tree automata for security protocol analysis. His work has produced significant contributions to reachability analysis, model checking, and the development of the TA4SP tool within the European AVISPA project. He has also contributed to projects like PROUVE and ACI SATIN, focusing on automated verification of cryptographic protocols.
His publication record shows consistent contributions to the field since 2004, with recent work (2024-2025) advancing SAT-based automated completion and equivalence class analysis in term rewriting systems. The trajectory of his research demonstrates a progression from foundational work on tree automata completion toward increasingly sophisticated approximation techniques for security protocol verification.
- A'Doc 2006: First award of the SPIM graduate school of the Franche-Comté University
As Head of MASTER MIAGE 1, Dr. BOICHUT oversees curriculum development and academic guidance. His research has been supported through multiple European projects including AVISPA (Automated Validation of Internet Security Protocols and Applications), where he contributed to the development of the TA4SP verification tool that handles algebraic properties of operators like exponentiation and exclusive or.
Within LIFO, he collaborates with the LMV team on theoretical computer science research, particularly in the areas of rewriting approximations and formal verification techniques applicable to both finite and infinite state systems.