2nd International School on Rewriting LORIA, Nancy, France July 2-6, 2007

- Research Interests -

• Automated Deduction with Equality,
• Strategies for Detecting Redundant Information,
• Constraints Solving,
• Verification of 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.
	Visit also the RTA Web Page (http://rewriting.loria.fr/rta/).
	And do not forget the IFIP Working Group 1.6 on Term Rewriting (http://rewriting.loria.fr/IFIP-WG1.6/).

- 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.

- Selected Publications -

[JRV06]

Tree Automata with Equality Constraints Modulo Equational Theories. In U. Furbach and N. Shankar, editors, Proceedings of 3rd International Joint Conference on Automated Reasoning, IJCAR, Seattle (WA), volume 4130 of Lecture Notes in Artificial Intelligence, pages 557-571. Springer, August 2006. (with F. Jacquemard and M. Rusinowitch)

[ABB+05]

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ò)

[CV04]

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)

[BTV03]

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

[CV02a]

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)

[JRV00b]

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)

[WV98]

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)

[Vig98]

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

[Vig95a]

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.

[RV95]

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

[Vig94b]

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.

[RV91]

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)

(complete list available here)

- PhD Thesis -

Université Henri Poincaré - Nancy 1 (November 1994).

Title: Automated Deduction with Symbolic Constraints in Equational Theories.

Supervisor: Michaël Rusinowitch.

Abstract / Résumé / Full Dissertation (in French).

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