Publications
On line reports/papers
on HAL
and on dblp
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
- [LGJ24] (pdf)
- T. Losekoot, T. Genet and T. Jensen. Verification of programs with ADTs using Shallow Horn Clauses.
In Proceedings of SAS'24. Volume 14995 of Lecture Notes in
Computer Science. Springer Verlag. 2024.
- [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.
Back to the Home Page