- Teaching Interests -

• 
• Master MIAGE: specialities ACSI, II, SID,
• Master Computer Science: speciality SIS (SIRAV),
• Licence MIASHS, specialities MIAGE and Cognitive Sciences

- Research Interests -

• Automated Deduction with Equality,
• Strategies for Detecting Redundant Information,
• Constraints Solving,
• Verification of Cryptographic Protocols,
• Efficient Implementation of Normalizing Techniques,
• Completeness Proofs,
• Non-classical Logics, Rough Sets.

Visit the Rewriting Home Page (http://rewriting.loria.fr/), realized with Nachum Dershowitz.

- Selected Publications -

[RV24]

Combined Abstract Congruence Closure for Theories with Associativity or Commutativity. In J. Bowles and H. Søndergaard, editors, 34th International Symposium Logic-Based Program Synthesis and Transformation, LOPSTR, Milan (Italy), volume 14919 of Lecture Notes in Computer Science, pages 82–98. Springer, September 2024. (with C. Ringeissen)

[ISSE10]

Formal Verification of Secure Group Communication Protocols Modelled in UML. Innovations in Systems and Software Engineering, 6: 125-133, 2010. (with P. Saqui-Sannes, T. Villemur, B. Fontan, S. Mota, M. S. Bouassida, N. Chridi, I. Chrisment)

[FAST08]

Automatic Methods for Analyzing Non-Repudiation Protocols with an Active Intruder. In P. Degano, J. Guttman and F. Martinelli, editors, Proceedings of the 5th International Workshop on Formal Aspects in Security and Trust (FAST), Malaga (Spain), October 9-10, 2008. Volume 5491 of Lecture Notes in Computer Science, pages 192-209. Springer, 2009. Selected paper. (with F. Klay)

[JLAP08]

Tree Automata with Equality Constraints Modulo Equational Theories. Journal of Logic and Algebraic Programming, 75(2): 182-208, April 2008. (with F. Jacquemard and M. Rusinowitch)

[CAV05]

The AVISPA Tool for the automated validation of internet security protocols and applications. In K. Etessami and S. Rajamani, editors, Proceedings of CAV'2005: 17th International Conference on Computer Aided Verification, Edinburgh, Scotland, volume 3576 of Lecture Notes in Computer Science, pages 281-285. Springer, July 2005. (with A. Armando, D. Basin, and Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.-C. Héam, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santos Santiago, M. Turuani and L. Viganò)

[ASE04]

Strategy for Verifying Security Protocols with Unbounded Message Size. Journal of Automated Software Engineering, 11(2): 141-166, April 2004. Kluwer Academic Publishers. (with Y. Chevalier)

[JAR03]

Abstract Congruence Closure. Journal of Automated Reasoning, 31(2): 129-168, January 2003. Kluwer Academic Publishers. (with L. Bachmair and A. Tiwari)

[CAV02a]

Automated Unbounded Verification of Security Protocols. In Ed Brinksma and Kim Guldstrand Larsen, editors, Proceedings of CAV'2002: 14th International Conference on Computer Aided Verification, Copenhaguen (Denmark), volume 2404 of Lecture Notes in Computer Science, pages 324-337. Springer, July 2002. (with Y. Chevalier)

[LPAR00]

Compiling and Verifying Security Protocols. In M. Parigot and A. Voronkov, editors, Proceedings of 7th Conference on Logic for Programming and Automated Reasoning (LPAR 2000), St Gilles (Reunion, France), volume 1955 of Lecture Notes in Computer Science, pages 131-160. Springer-Verlag, November 2000. (with F. Jacquemard and M. Rusinowitch)

[RSKD98]

Rough Algebras and Automated Deduction. In L. Polkowski and A. Skowron, editors, Rough Sets in Knowledge Discovery 1, pages 261-275. Springer Verlag, July 1998. (with A. Wasilewska)

[FI98]

Automated Deduction Techniques for Studying Rough Algebras. Fundamenta Informaticae, 33(1):85-103, February 1998.

[CSL95]

Positive Deduction modulo Regular Theories. In H.K. Büning, editor, Proceedings of the Annual Conference of the European Association for Computer Science Logic, Paderborn (Germany), volume 1092 of Lecture Notes in Computer Science, pages 468-485, September 1995. Springer-Verlag. Selected paper.

[AAECC95]

Automated Deduction with Associative and Commutative Operators. Applicable Algebra in Engineering, Communication and Computing, 6(1):23-56, January 1995. (with M. Rusinowitch)

[CADE94]

Associative-Commutative Deduction with Constraints. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, Nancy (France), volume 814 of Lecture Notes in Artificial Intelligence, pages 530-544. Springer-Verlag, June 1994.

[FAIR91]

Automated Deduction with Associative Commutative Operators. In Ph. Jorrand and J. Kelemen, editors, Fundamentals of Artificial Intelligence Research, Smolenice (Czechoslovakia), Volume 535 of Lecture Notes in Computer Science, pages 185-199, September 1991. Springer-Verlag. (with M. Rusinowitch)

- Habilitation and PhD Theses -

[HDR]

Automated Deduction applied to the Analysis and Verification of Infinite State Systems. (in French)
Habilitation à diriger des recherches of the University Nancy 2, November 2011.
Jury: Laurent Fribourg (president), Bernhard Gramlich (reviewer), Christopher Lynch (reviewer), Paliath Narendran, Michaël Rusinowitch, Peter Ryan, Jeanine Souquières, Ralf Treinen (reviewer).

[PhD Thesis]

Automated Deduction with Symbolic Constraints in Equational Theories. (in French)
PhD Thesis of the University Henri Poincaré, Novembre 1994.
Jury: Ricardo Caferra, Philippe Jorrand (reviewer), Jean-Pierre Jouannaud (president), Hélène Kirchner, Michaël Rusinowitch (supervisor), René Schott (reviewer), Wayne Snyder (reviewer).

- daTac -

daTac is a theorem prover implementing the deduction techniques I have developped, for first-order logic with equality and AC symbols. For more information, see the official daTac Home Page.

*** Come to France *** *** Visit Nancy! *** *** Visit the Lorraine! ***
	The famous Ecole de Nancy