Publications

Journals

[GS17] (pdf)

T. Genet and Y. Salmon. Reachability Analysis of Innermost Rewriting -- extended version. Logical Methods in Computer Science. Vol 13(1). pp. 1-35 pages. 2017.

[Genet16] (pdf)

T. Genet. Termination Criteria for Tree Automata Completion. In Journal of Logical and Algebraic Methods in Programming. Volume 85, Issue 1, Part 1, pages 3-33. 2016.

[GR10] (pdf)

T. Genet and V. Rusu. Equational Tree Automata Completion. In Journal of Symbolic Computation. Volume 45. 26 pages. 2010. 

[FGV04] (gzipped)

G. Feuillade, T. Genet and V. Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. In Journal of Automated Reasoning. Volume 33 (3-4). 49 pages. 2004.

Conferences

[LGJ23] (pdf)

T. Losekoot, T. Genet and T. Jensen. Automata-based verification of relational properties of functions over data structures. In Proceedings of FSCD'23. Volume 260 of LIPIcs, Schloss Dagstuhl. 2023.

[HGJ20] (pdf)

T. Haudebourg, T. Genet and T. Jensen. Regular Language Type Inference with Term Rewriting. In Proceedings of ICFP'20. ACM, 2020.

[GJS20] (pdf)

T. Genet, T. Jensen and J. Sauvage. Termination of Ethereum's Smart Contracts. In Proceedings of SECRYPT'20. SciTePress, 2020.

[Gen18] (pdf)

T. Genet. Completeness of Tree Automata Completion. In Proceedings of FSCD'18. Volume 108 of LIPIcs, Schloss Dagstuhl. 2018.

[GHJ18] (pdf)

T. Genet, T. Haudebourg and T. Jensen. Verifying Higher-Order Functions with Tree Automata. In Proceedings of FoSSaCS'18. Volume 10803 Lecture Notes in Computer Science. Springer Verlag, 2018.

[GS15] (pdf)

T. Genet and Y. Salmon. Reachability Analysis of Innermost Rewriting. In Proceedings of RTA'15. LIPIcs 36, Schloss Dagstuhl. 2015.

[GLLGM13] (pdf)

T. Genet, T. Le Gall, A. Legay and V. Murat.A Completion Algorithm for Lattice Tree Automata. In Proceedings of CIAA'13, volume 7982 of Lecture Notes in Computer Science, pages 134-145. Springer-Verlag, 2013.

[BBGL12] (pdf)

Y. Boichut, B. Boyer, T. Genet and A. Legay. Equational Abstraction Refinement for Certified Tree Regular Model Checking. In Proceedings of ICFEM'12, volume 7635 of Lecture Notes in Computer Science, pages 299-315. Springer-Verlag, 2012.

[BGJ08] (pdf)

B. Boyer, T. Genet and T. Jensen. Certifying a Tree Automata Completion Checker. In Proceedings of IJCAR'08, volume 5195 of Lecture Notes in Computer Science. Springer-Verlag, 2008.

[BBGM08] (pdf)

Y. Boichut, E. Balland, T. Genet and P.-E. Moreau. Towards an Efficient Implementation of Tree Automata Completion. In Proceedings of AMAST'08, volume 5140 of Lecture Notes in Computer Science. Springer-Verlag, 2008.

[BGGH07] (pdf)

Y. Boichut, T. Genet, Y. Glouche and O. Heen. Using Animation to Improve Formal Specifications of Security Protocols. In Proceedings of SAR-SSI'07, 2007.

[BGJL07] (pdf)

Y. Boichut, T. Genet, T. Jensen and L. Le Roux. Rewriting Approximations for Fast Prototyping of Static Analyzers. In Proceedings of 18th International Conference on Rewriting Techniques and Applications, volume 4533 of Lecture Notes in Computer Science. Springer-Verlag, 2007.

[BG06] (pdf or .ps gzipped)

Y. Boichut and T. Genet. Feasible Trace Reconstruction for Rewriting Approximations. In Proceedings of 17th International Conference on Rewriting Techniques and Applications, Seattle (USA), volume 4098 of Lecture Notes in Computer Science. Springer-Verlag, 2006.

[GT01] (gzipped or not)

T. Genet and V. Viet Triem Tong. Reachability Analysis of Term Rewriting Systems with Timbuk. In Proceedings 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Havana (Cuba), volume 2250 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2001.

[GK00] (gzipped)

T. Genet and F. Klay. Rewriting for Cryptographic Protocol Verification. In Proceedings 17th International Conference on Automated Deduction, Pittsburgh (Pen., USA), volume 1831 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2000.

[Gen98a] (zipped or not)

T. Genet. Decidable approximations of sets of descendants and sets of normal forms. In T. Nipkow, editor, Proceedings 9th International Conference on Rewriting Techniques and Applications, Tsukuba (Japan), volume 1379 of Lecture Notes in Computer Science, pages 151-165. Springer-Verlag, 1998.

[GG97a] (zipped or not)

T. Genet and I. Gnaedig. Termination proofs using gpo ordering constraints. In M. Dauchet, editor, Proceedings 22nd International Colloquium on Trees in Algebra and Programming, Lille (France), volume 1214 of Lecture Notes in Computer Science, pages 249-260. Springer-Verlag, 1997.

Workshops

[GGHL18] (pdf)

T. Genet, T. Gillard, T. Haudebourg, S. Lê Cong. Extending Timbuk to Verify Functional Programs. In Proceedings of WRLA'18, volume 11152 of Lecture Notes in Computer Science. Springer-Verlag, 2018.

[Gen14] (pdf)

T. Genet. Towards Static Analysis of Functional Programs using Tree Automata Completion. In Proceedings of WRLA'14, volume 8663 of Lecture Notes in Computer Science. Springer-Verlag, 2014.

[GS12] (pdf)

T. Genet, Y. Salmon. Proving Reachability Properties on Term Rewriting Systems with Strategies. In 2nd Joint International Workshop on Strategies in Rewriting, Proving and Programming, (IJCAR'12 workshop), 2012.

[HGG09] (pdf)

O. Heen, G. Guette, T. Genet. On the unobservability of a trust relation in mobile ad hoc networks. In Proc. of WISTP'09, Brussels, volume 5746 of Lecture Notes in Computer Science, Springer, 2009.

[BG09] (pdf)

B. Boyer, T. Genet. Verifying Temporal Regular properties of Abstractions of Term Rewriting Systems. In Proc. of RULE'09, Brasilia, volume 21 of Electronic Proceedings in Theoretical Computer Science. June 2009.

[HGGP08] (pdf)

O. Heen, T. Genet, S. Geller and N. Prigent. An Industrial and Academic Joint Experiment on Automated Verification of a Security Protocol. In IFIP Networking  Workshop on Mobile and Networks Security, Singapore, May 2008.

[GGHC06] (pdf)

Y. Glouche, T. Genet, O. Heen and O. Courtay. A Security Protocol Animator Tool for AVISPA. In ARTIST2 Workshop on Security Specification and Verification of Embedded Systems , Pisa, May 2006.

[FG03] (gzipped)

G. Feuillade and T. Genet. Reachability in Conditional Term Rewriting Systems. In Proc. of FTP'03, Workshop on First Order Theorem Proving , Electr. Notes Theor. Comput. Sci., volume 86, No 1. May 2003.

[GJKP03] (gzipped)

T. Genet, T. Jensen, V. Kodati and D. Pichardie. A JavaCard CAP Converter in PVS. In Proc. of COCV'03, Workshop on Compiler Optimization Meets Compiler Verification, volume 82 of ENTCS, No 2, April 2003.

[GTTT03] (gzipped)

T. Genet, Y.-M. Tang-Talpin, and V. Viet Triem Tong. Verification of copy-protection cryptographic protocol using approximations of term rewriting systems. In Proc. of WITS'03, Workshop on Issues in the Theory of Security, 2003.

Tutorials

[G17] (link on the video)

T. Genet. SPAN+AVISPA for Verifying Cryptographic Protocols. 2017.

[Gen15a] (pdf)

T. Genet. A Short Isabelle/HOL Tutorial for the Functional Programmer. Technical Report, Inria, 2015.

[Gen15b] (pdf)

T. Genet. A Short SPAN+AVISPA Tutorial. Technical Report, Inria, 2015.

French Journals

[G08] (link)

T. Genet. Le protocole cryptographique de paiement par carte bancaire. In Interstices, Février 2008.

[HGH08] (pdf)

O. Heen, T. Genet, E. Houssay. Votre protocole est-il vérifié? In MISC 39, p 58--68, Septembre 2008.

French Workshops

[GKV15] (pdf)

T. Genet, B. Kordy and A. Vansyngel. Vers un outil de vérification formelle légère pour OCaml. In AFADL'15. Juin 2015.

Posters

[RAVAJ08] (pdf)

RAVAJ Team. Réécriture pour la vérification d'applications Java. In Journées du GDR Génie de la Programmation et du Logiciel (GPL), Toulouse, Janvier 2009.

Technical Reports

[Gen15a] (pdf)

Thomas Genet. A Short Isabelle/HOL Tutorial for the Functional Programmer. Technical Report, Inria, 2015.

[Gen15b] (pdf)

Thomas Genet. A Short SPAN+AVISPA Tutorial. Technical Report, Inria, 2015.

[BGJ08] (pdf)

Benoît Boyer, Thomas Genet and Thomas Jensen. Certifying a Tree Automata Completion Checker. Technical Report RR-6462, INRIA, 2008.

[BGJL06] (pdf, ps gzipped)

Yohan Boichut, Thomas Genet, Thomas Jensen and Luka Leroux. Rewriting Approximations for Fast Prototyping of Static Analyzers. Technical Report RR-5997, INRIA, 2006.

[FGT03] (gzipped)

Guillaume Feuillade, Thomas Genet and Valérie Viet Triem Tong. Reachability Analysis of Term Rewriting Systems. Technical Report RR-4970, INRIA, 2003.

[GT02] (gzipped)

Thomas Genet and Valérie Viet Triem Tong. Proving Negative Conjectures on Equational Theories using Induction and Abstract Interpretation. Technical Report RR-4576, INRIA, 2002.

[GT01] (gzipped, or not)

Thomas Genet and Valérie Viet Triem Tong. Reachability Analysis of Term Rewriting Systems with Timbuk (extended version). Technical Report RR-4266, INRIA, 2001.

[GK00] (zipped, gzipped or not)

Thomas Genet and Francis Klay. Rewriting For Cryptographic Protocol Verification (extended version). Technical Report RR-3921, INRIA, 2000.

[Gen97a] (zipped or not)

Thomas Genet. Proving Termination of Sequential Reduction Relation using Tree Automata. Technical report, CRIN, 1997. 97-R-091.

[Gen97b] (zipped or not)

Thomas Genet. Decidable approximations of sets of descendants and sets of normal forms (extended version). Technical Report RR-3325, Institut National de Recherche en Informatique et Automatique, 1997.

[GG97b] (zipped or not)

Thomas Genet and Isabelle Gnaedig. Termination proofs using gpo ordering constraints (extended version). Technical report, Institut National de Recherche en Informatique et Automatique, 1997. RR-3087.

Habilitation Thesis

[Gen09] (pdf)

Thomas Genet. Reachability analysis of rewriting for software verification. Habilitation à diriger des recherches, Université de Rennes 1, 2009.

PhD Thesis

[Gen98b] (zipped, gzipped or not)

Thomas Genet. Contraintes d'ordre et automates d'arbres pour les preuves de terminaison. Thèse de Doctorat d'Université, Université Henri Poincaré - Nancy 1, 1998.