Publications

* Habilitation and PhD Theses

[Vig11]
L. Vigneron. Déduction automatique appliquée à l'analyse et la vérification de systèmes infinis. Habilitation à diriger des recherches de l'Université Nancy 2, novembre 2011.
[Vig94f]
L. Vigneron. Déduction automatique avec contraintes symboliques dans les théories équationnelles. Thèse de Doctorat de l'Université Henri Poincaré - Nancy I, novembre 1994.

* Journals

[Sall10]
P. Saqui-Sannes, T. Villemur, B. Fontan, S. Mota, M. S. Bouassida, N. Chridi, I. Chrisment and L. Vigneron. Formal Verification of Secure Group Communication Protocols Modelled in UML. Innovations in Systems and Software Engineering, 6: 125-133, 2010.
[LV10]
J. Liu and L. Vigneron. Design and Verification of a Non-Repudiation Protocol Based on Receiver-Side Smart Card. IET Information Security, 4(1): 15-29, March 2010.
[JRV08]
F. Jacquemard, M. Rusinowitch and L. Vigneron. Tree Automata with Equality Constraints Modulo Equational Theories. Journal of Logic and Algebraic Programming, 75(2): 182-208, April 2008.
[BCCFV07]
M. S. Bouassida, N. Chridi, I. Chrisment, O. Festor and L. Vigneron. Automated Verification of a Key Management Architecture for Hierarchical Group Protocols. Annals of Telecommunications, 62(11-12): 1365-1387, November-December 2007.
[CV06a]
N. Chridi and L. Vigneron. Sécurité des communications de groupe. Revue de l'Électricité et de l'Électronique, 6/7: 51-60, juin/juillet 2006. Société de l'Électricité, de l'Électronique et des Technologies de l'Information et de la Communication.
[CV04a]
Y. Chevalier and L. Vigneron. Strategy for Verifying Security Protocols with Unbounded Message Size. Journal of Automated Software Engineering, 11(2): 141-166, April 2004. Kluwer Academic Publishers.
[BTV03]
L. Bachmair, A. Tiwari and L. Vigneron. Abstract Congruence Closure. Journal of Automated Reasoning, 31(2): 129-168, January 2003. Kluwer Academic Publishers.
[Vig98]
L. Vigneron. Automated Deduction Techniques for Studying Rough Algebras. Fundamenta Informaticae, 33(1): 85-103, February 1998.
[RV95]
M. Rusinowitch and L. Vigneron. Automated Deduction with Associative and Commutative Operators. Applicable Algebra in Engineering, Communication and Computing, 6(1):23-56, January 1995.

* Books/Proceedings as Editor

[Vig05a]
L. Vigneron, editor. Proceedings of the 19th International Workshop on Unification, held during RDP'2005 in Nara, Japan, April 2005.
Available as LORIA Research Report A05-R-022, Nancy, France.
[KV04]
D. Kapur and L. Vigneron, editors. Special issue on First-Order Theorem Proving of the Journal of Automated Reasoning, Volume 33, Numbers 3-4, Springer Science+Business Media B.V., October 2004. ISSN: 0168-7433 (Paper) 1573-0670 (Online).
[DV03]
I. Dahn and L. Vigneron, editors. FTP'2003, 4th International Workshop on First-Order Theorem Proving. Volume 86, Issue 1 of Electronic Notes in Theoretical Computer Science (ENTCS), Elsevier Science, June 2003.
Preliminary version available as Technical Report DSIC-II/10/03, Universidad Politécnica de Valencia, 2003.

* In Book

[CV07]
N. Chridi and L. Vigneron. Strategy for Flaws Detection based on a Services-driven Model for Group Protocols. In Frédéric Benhamou, Narendra Jussien and Barry O'Sullivan, editors, Future and Trends in Constraint Programming, chapter 24, pages 361-370, April 2007. ISTE.
[WV98]
A. Wasilewska and L. Vigneron. 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.

* Conferences

[RV24b]
R. Ringeissen and L. Vigneron. 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.
[Vig13]
L. Vigneron. Déduction automatique appliquée à l'analyse et la vérification de systèmes infinis (conférence invitée). Dans J. Souquières et V. Wiels, éditeurs, Approches Formelles dans l'Assistance au Développement de Logiciels, AFADL, Nancy (France), avril 2013.
[JRV06]
F. Jacquemard, M. Rusinowitch and L. Vigneron. 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.
[BCCFV06]
M. S. Bouassida, N. Chridi, I. Chrisment, O. Festor and L. Vigneron. Automatic Verification of a Key Management Architecture for Hierarchical Group Protocols. In F. Cuppens and H. Debar, editors, Proceedings of 5th Conference on Security and Network Architectures, SAR, pages 381-397, Seignosse (France), June 2006.
[BKV06]
Y. Boichut, N. Kosmatov and L. Vigneron. Validation of Prouve Protocols using the Automatic Tool TA4SP. In Proceedings of 3rd Taiwanese-French Conference on Information Technology, TFIT, pages 467-480, Nancy (France), March 2006.
[SV06]
J. Santiago and L. Vigneron. Automatically Analysing Non-repudiation with Authentication. In Proceedings of 3rd Taiwanese-French Conference on Information Technology, TFIT, pages 541-554, Nancy (France), March 2006.
[SV05]
J. Santiago et L. Vigneron. Study for Automatically Analysing Non-repudiation. Dans les actes du 1er Colloque sur les Risques et la Sécurité d'Internet et des Systèmes, CRiSIS, pages 157-171, Bourges (France), octobre 2005.
[CV05]
N. Chridi et L. Vigneron. Modélisation des propriétés de sécurité de protocoles de groupe. Dans les actes du 1er Colloque sur les Risques et la Sécurité d'Internet et des Systèmes, CRiSIS, pages 119-132, Bourges (France), octobre 2005. Élu meilleur papier de la conférence.
[ABB+05]
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, L. Viganò, and L. Vigneron. 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.
[Vig05b]
L. Vigneron. A Tool helping to Design Cryptographic Protocols (tutorial). In 4th Conference on Security and Network Architectures (SAR'05), Batz sur Mer, France, June 2005.
[CKRTV03]
Y. Chevalier, R. Küsters, M. Rusinowitch, M. Turuani and L. Vigneron. Extending the Dolev-Yao Intruder for Analyzing an Unbounded Number of Sessions. In Matthias Baaz, editor, Proceedings of Computer Science Logic (CSL 03) and 8th Kurt Gödel Colloquium (8th KCG), Vienna (Austria), volume 2803 of Lecture Notes in Computer Science, pages 128-141. Springer, August 2003.
[CV02a]
Y. Chevalier and L. Vigneron. 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.
[ABB+02]
A. Armando, D. Basin, M. Bouallagui, Y. Chevalier, L. Compagna, S. Mödersheim, M. Rusinowitch, M. Turuani, L. Viganò and L. Vigneron. The AVISS Security Protocol Analysis Tool. 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 349-353. Springer, July 2002. Tool presentation.
[CV01a]
Y. Chevalier and L. Vigneron. A Tool for Lazy Verification of Security Protocols (short paper). Proceedings of ASE-2001: The 16th IEEE Conference on Automated Software Engineering, Coronado (CA), pages 373-376. IEEE Computer Society Press, November 2001.
[JRV00b]
F. Jacquemard, M. Rusinowitch and L. Vigneron. 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.
[BRTV00b]
L. Bachmair, I. V. Ramakrishnan, A. Tiwari and L. Vigneron. Congruence Closure Modulo Associativity and Commutativity. In H. Kirchner and Ch. Ringeissen, editors, Proceedings of 3rd International Workshop on Frontiers of Combining Systems (FroCoS 2000), Nancy (France), volume 1794 of Lecture Notes in Artificial Intelligence, pages 245-259. Springer-Verlag, March 2000.
[VW99]
L. Vigneron and A. Wasilewska. Rough Sets based Proofs Visualisation. In R. N. Davé and T. Sudkamp, editors, Proceedings of the 18th International Conference of the North American Fuzzy Information Processing Society (NAFIPS'99), invited session on Granular Computing and Rough Sets, New York City (New York), pages 805-808. IEEE, June 1999.
[VW98a]
L. Vigneron and A. Wasilewska. Rough Sets Congruences and Diagrams. In R. Slowinski, editor, Proceedings of the 16th European Conference on Operational Research (EURO XVI), session on Rough Sets, Brussels (Belgium), July 1998. (abstract)
[Vig96c]
L. Vigneron. Automated Reasoning in Equational Theories. Symposium of Logic, Algebra and Computer Science, Helena Rasiowa in memoriam, Warsaw (Poland), December 1996 (4 pages).
[VW96a]
L. Vigneron and A. Wasilewska. Rough and Modal Algebras. In P. Borne, editor, Proceedings of the IMACS/IEEE CESA'96 International Multiconference (Computational Engineering in Systems Applications), Symposium on Modelling, Analysis and Simulation, Lille (France), pages 1107-1112, July 1996.
[Vig95b]
L. Vigneron. 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.
[Vig94d]
L. Vigneron. Associative-Commutative Deduction with Constraints. In A. Bundy, editor, Proceedings of the 12th Conference on Automated Deduction, Nancy (France), volume 814 of Lecture Notes in Artificial Intelligence, pages 530-544. Springer-Verlag, June 1994.
[RV91]
M. Rusinowitch and L. Vigneron. 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.

* Workshops

[RV24a]
R. Ringeissen and L. Vigneron. Combined Abstract Congruence Closure for Associative or Commutative Theories. In S. Escobar and O. Fernandez Gil, editors, 38th International Workshop on Unification, UNIF, Nancy (France), July 2024.
[Sall09]
P. Saqui-Sannes, T. Villemur, B. Fontan, S. Mota, M. S. Bouassida, N. Chridi, I. Chrisment and L. Vigneron. UML Modeling and Formal Verification of Secure Group Communication Protocols. Second IEEE international workshop on UML and Formal Methods, Rio de Janeiro, Brazil. 2009.
[KV08]
F. Klay and L. Vigneron. 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.
[SV07]
J. Santiago and L. Vigneron. Optimistic Non-repudiation Protocol Analysis. In D. Sauveron et al., editors, Proceedings of the Workshop in Information Security Theory and Practices (WISTP), Smart Cards, Mobile and Ubiquitous Computing Systems, Heraklion (Greece), volume 4462 of Lecture Notes in Computer Science, pages 90-101. Springer, May 2007.
[CV06b]
N. Chridi and L. Vigneron. Strategy for Flaws Detection based on a Services-driven Model for Group Protocols. In Benjamin Blanc, Arnaud Gotlieb and Claude Michel, editors, Proceeding of the Workshop on Constraints in Software Testing, Verification and Analysis, Nantes (France), pages 88-99, September 2006.
[CheAll04]
Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, J. Mantovani, S. Mödersheim and L. Vigneron. A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols. Proceedings of Workshop on Specification and Automated Processing of Security Requirements (SAPS), Linz (Austria), September 2004.
[Vig04]
L. Vigneron. Automatic Verification of Security Protocols. 18th Int. Workshop on Unification, Cork (Ireland), July 2004. Invited talk.
[CV04b]
Y. Chevalier and L. Vigneron. Rule-based Programs describing Internet Security Protocols. In S. Abdennadher and C. Ringeissen, editors, Proceedings of the 5th Int. Workshop on Rule-Based Programming (RULE), Aachen (Germany), June 2004. Volume 124.1, pages 113-132, of Electronic Notes in Theoretical Computer Science, Elsevier Science Publishers.
[BCR+02]
M. Bouallagui, Y. Chevalier, M. Rusinowitch, M. Turuani and L. Vigneron. Analyse Automatique de Protocoles de Sécurité avec CASRUL. Actes de SAR'2002 Sécurité et Architecture Réseaux, Marrakech (Maroc), Juillet 2002.
[CV01b]
Y. Chevalier and L. Vigneron. Towards Efficient Automated Verification of Security Protocols. Proceedings of the Verification Workshop (VERIFY'01) (in connection with IJCAR'01), Siena (Italy), June 2001. Universit\`a degli studi di Siena, TR DII 08/01, pages 19-33.
[BRTV00a]
L. Bachmair, I. V. Ramakrishnan, A. Tiwari and L. Vigneron. Abstract Congruence Closure for Normalization. First International Workshop FreGe 2000, Genova (Italy), February 2000.
[JRV00a]
F. Jacquemard, M. Rusinowitch and L. Vigneron. Narrowing Semantics for Cryptographic Protocols and Verification. First International Workshop FreGe 2000, Genova (Italy), February 2000.
[WLV99]
A. Wasilewska, M. Lifantsev and L. Vigneron. A Decision Procedure for Proofs Visualisation. In Ewa Orlowska, editor, session of the Polish Association for Logic and Philosophy of Science dedicated to the memory of Andrzej Mostowski and Helena Rasiowa, Warsaw (Poland), November 1999.
[VW98b]
L. Vigneron and A. Wasilewska. Rough Diagrams. Proceedings of the sixth Workshop on Rough Sets, Data Mining and Granular Computing (RSDMGrC'98) at the 4th Joint Conference on Information Sciences, Research Triangle Park (North Carolina), October 1998.
[Vig97a]
L. Vigneron. Automated Deduction and Rough Information. 4th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice. AISB-97, Manchester (England), April 1997.
[WV97]
A. Wasilewska and L. Vigneron. On Generalized Rough Sets. Proceedings of the 5th Workshop on Rough Sets and Soft Computing (RSSC'97) at the 3rd Joint Conference on Information Sciences, Research Triangle Park (North Carolina), March 1997.
[BRV96]
L. Bachmair, I. V. Ramakrishnan and L. Vigneron. Efficient Term Rewriting Techniques. In M. Rodriguez-Artalejo, editor, Proceedings of the CCL'96 Workshop, San Lorenzo (Spain), September 1996.
[VW96b]
L. Vigneron and A. Wasilewska. Automated Study of Rough and Modal Algebras. In M. Rodriguez-Artalejo, editor, Proceedings of the CCL'96 Workshop, San Lorenzo (Spain), September 1996.
[Vig96a]
L. Vigneron. Extended Equations for Deduction modulo E. In M. Rodriguez-Artalejo, editor, Proceedings of the CCL'96 Workshop, San Lorenzo (Spain), September 1996.
[WV95]
A. Wasilewska and L. Vigneron. Rough Equality Algebras. Proceedings of the Workshop on Rough Set Theory (RST'95), at the 2nd Joint Conference on Information Sciences, Wrightsville Beach (North Carolina), September 1995.
[Vig95a]
L. Vigneron. Efficient Strategies for Automated Reasoning. In A. Ireland, editor, Proceedings of the 2nd Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice. AISB-95, Sheffield (England), April 1995.
[KV94]
H. Kirchner and L. Vigneron. Deduction with Constraints for Theory Reasoning; Completeness and Simplification Problems. In U. Furbach, editor, Proceedings of the Workshop on Theory Reasoning in Automated Deduction. CADE-94, Nancy (France), June 1994.
[Vig94c]
L. Vigneron. Proofs in Equational Theories. In D. Lugiez, editor, Proceedings of the 8th Workshop on Unification, Le Val d'Ajol (France), June 1994.
[Vig93]
L. Vigneron. Basic AC-Paramodulation. In F. Orejas, editor, Proceedings of the 2nd CCL Workshop, L'Escala (Spain), September 1993.
[RV92]
M. Rusinowitch and L. Vigneron. Associative Commutative Deduction. In E. Domenjoud and C. Kirchner, editors, Proceedings of the 1st CCL Workshop, Le Val d'Ajol (France), October 1992.

* National Workshops

[Vig23]
L. Vigneron. L'IA au service de la sécurité des communications. Intelligence artificielle au sein des organisations apprenantes (intelligentes ?), Longwy, juillet 2023.
[Vig13]
L. Vigneron. Déduction automatique appliquée à l'analyse et la vérification de systèmes infinis. Approches Formelles dans l'Assistance au Développement de Logiciels, AFADL 2013, Nancy, avril 2013.
[Vig99]
L. Vigneron. Clôture par congruence modulo associativité et commutativité. Journée du groupe LODeC (Langages et Outils pour la Déduction sous Contraintes) du G.D.R. Algorithmique, Langage et Programmation, Paris, décembre 1999.
[Vig94g]
L. Vigneron. Déduction automatique modulo une théorie équationnelle régulière. Journées du P.R.C. Mécanisation du Raisonnement, Chamrousse, novembre 1994.
[Vig94e]
L. Vigneron. Déduction dans les théories équationnelles avec contraintes symboliques. Journées du G.D.R. Programmation, Lille, septembre 1994.
[Vig94a]
L. Vigneron. Déduction associative-commutative avec contraintes. Journées du P.R.C. Mécanisation du Raisonnement, Toulouse, février 1994.

* Softwares

* AVISPA Tool: a free tool for Automated Validation of Internet Security Protocols and Applications.

* AVISS: a tool for Automated Validation of Infinite-State Systems.

* CASRUL: a system for automatic verification of cryptographic protocols.

*Abstract CC

[TV00a]
A. Tiwari and L. Vigneron. Implementation of Abstract Congruence Closure with randomly generated CC problem instances (gzipped tar file).

* System Presentations of daTac

[Vig97b]
L. Vigneron. daTac. International Conference TABLEAUX'97 - Analytic Tableaux and Related Methods, Abbaye des Prémontrés, Pont-à-Mousson (France), May 1997.
[Vig96b]
L. Vigneron. Déduction automatique avec contraintes en daTac. Journées du G.D.R. Programmation, Orléans, Novembre 1996.

* Unpublished Research Reports

[KSV07]
F. Klay, J. Santiago and L. Vigneron. Automatic Methods for Analyzing Non-Repudiation Protocols with an Active Intruder. Research Report 6324, INRIA, October 2007. (19 pages)
[Vig95c]
L. Vigneron. Theorem Proving Modulo Regular Theories. Research Report 95/1, Department of Computer Science, State University of New York at Stony Brook, Stony Brook, January 1995. (15 pages)
[Vig94b]
L. Vigneron. Superposition in AC Theories : Proof of Completeness by Semantic Trees. Internal report 94-R-045, Centre de Recherche en Informatique de Nancy, Vandoeuvre-lès-Nancy, March 1994. (24 pages)
[Hist92]
P. Wolff, L. Vigneron, C. Ringeissen, O. Perrin, J. L. Moysset, O. Hermann, R. Curien, N. Brown et L. Andrey. Un bref historique de l'informatique. Rapport interne 92-R-159, Centre de Recherche en Informatique de Nancy, Vandoeuvre-lès-Nancy, 1992. (19 pages)
[Vig90]
L. Vigneron. Déduction Automatique dans des Théories Associatives-Commutatives. Rapport de D.E.A. Rapport interne 90-R-183, Centre de Recherche en Informatique de Nancy, Vandoeuvre-lès-Nancy, 1990. (100 pages)