Publications HAL de Thomas,Genet

2020

Journal articles

titre
Regular Language Type Inference with Term Rewriting - extended version
auteur
Timothée Haudebourg, Thomas Genet, Thomas Jensen
article
Proceedings of the ACM on Programming Languages, ACM, 2020, International Conference on Functional Programming (ICFP), 4 (ICFP), pp.1-29. ⟨10.1145/3408994⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02795484/file/report%20%281%29.pdf BibTex

Conference papers

titre
Termination of Ethereum’s Smart Contracts
auteur
Thomas Genet, Thomas Jensen, Justine Sauvage
article
SECRYPT 2020 - 17th International Conference on Security and Cryptography, Jul 2020, Lieusaint - Paris / Virtual, France. pp.39-51, ⟨10.5220/0009564100390051⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-03122008/file/main.pdf BibTex

Reports

titre
Termination of Ethereum's Smart Contracts
auteur
Thomas Genet, Thomas Jensen, Justine Sauvage
article
[Research Report] Univ Rennes, Inria, CNRS, IRISA. 2020
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-02555738/file/reportInria.pdf BibTex

2018

Conference papers

titre
Completeness of Tree Automata Completion
auteur
Thomas Genet
article
FSCD 2018 - 3rd International Conference on Formal Structures for Computation and Deduction, Jul 2018, Oxford, United Kingdom. pp.1-20, ⟨10.4230/LIPIcs.FSCD.2018.15⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01778407/file/Genet-FSCD18.pdf BibTex
titre
Vérifier des fonctions d'ordre supérieur à l'aide d'automates d'arbre
auteur
Thomas Genet, Timothée Haudebourg, Thomas Jensen
article
17èmes Journées AFADL 2018 - Approches Formelles dans l'Assistance au Développement de Logiciels, May 2018, Grenoble, France. pp.1-3
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01790916/file/paper.pdf BibTex
titre
Automata and Equations based Approximations for Reachability Analysis
auteur
Thomas Genet
article
WRLA 2018 - 12th International Workshop on Rewriting Logic and its Applications, Apr 2018, Thessalonique, Greece. pp.1
Accès au bibtex
BibTex
titre
Extending Timbuk to Verify Functional Programs
auteur
Thomas Genet, Tristan Gillard, Timothée Haudebourg, Sébastien Cong
article
WRLA 2018 - 12th International Worshop on Rewriting Logic and its Applications, Apr 2018, Thessalonique, Greece. pp.153-163, ⟨10.1007/978-3-319-99840-4_9⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01775190/file/main.pdf BibTex
titre
Verifying Higher-Order Functions with Tree Automata
auteur
Thomas Genet, Timothée Haudebourg, Thomas Jensen
article
FoSSaCS 2018 - 21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. pp.565-582, ⟨10.1007/978-3-319-89366-2_31⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01775188/file/GenetHJ-FOSSACS18.pdf BibTex

2017

Journal articles

titre
Reachability Analysis of Innermost Rewriting - extended version
auteur
Thomas Genet, Yann Salmon
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2017, ⟨10.2168/LMCS-???⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01532090/file/main.pdf BibTex

Conference papers

titre
GPFinder: Tracking the Invisible in Android Malware
auteur
Mourad Leslous, Valérie Viet Triem Tong, Jean-François Lalande, Thomas Genet
article
12th International Conference on Malicious and Unwanted Software, Oct 2017, Fajardo, Puerto Rico. pp.39-46, ⟨10.1109/MALWARE.2017.8323955⟩
Accès au texte intégral et bibtex
https://hal-centralesupelec.archives-ouvertes.fr/hal-01584989/file/camera.pdf BibTex

Other publications

titre
SPAN+AVISPA for Verifying Cryptographic Protocols
auteur
Thomas Genet
article
2017
Accès au bibtex
BibTex

Reports

titre
Verifying Higher-Order Functions with Tree Automata: Extended Version
auteur
Thomas Genet, Timothée Haudebourg, Thomas Jensen
article
[Technical Report] Irisa. 2017, pp.1-20
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01614380/file/Verifying%20Higher-Order%20Functions%20with%20Tree%20Automata.pdf BibTex
titre
Automata Completion and Regularity Preservation
auteur
Thomas Genet
article
[Research Report] IRISA, Inria Rennes. 2017
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01501744/file/mainLong.pdf BibTex
titre
A Short Isabelle/HOL Tutorial for the Functional Programmer
auteur
Thomas Genet, Jørgen Villadsen
article
[Research Report] IRISA. 2017, pp.1-5
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01208577/file/main.pdf BibTex

2016

Journal articles

titre
Termination criteria for tree automata completion
auteur
Thomas Genet
article
Journal of Logical and Algebraic Methods in Programming, Elsevier, 2016, 85, Issue 1, part 1, pp.3-33. ⟨10.1016/j.jlamp.2015.05.003⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01194533/file/Genet-JLAMP15.pdf BibTex

2015

Conference papers

titre
Kharon : Découvrir, comprendre et reconnaître des malware Android par suivi de flux d'information
auteur
Radoniaina Andriatsimandefitra Ratsisahanana, Thomas Genet, Laurent Guillo, Jean-François Lalande, David Pichardie, Valérie Viet Triem Tong
article
Rendez-vous de la Recherche et de l'Enseignement de la Sécurité des Systèmes d'Information, May 2015, Troyes, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01154368/file/kharon.pdf BibTex
titre
Vers un outil de vérification formelle légere pour OCaml
auteur
Thomas Genet, Barbara Kordy, Amaury Vansyngel
article
AFADL, 2015, Bordeaux, France. pp.6
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01194538/file/GenetKordyVansyngel-AFADL15.pdf BibTex
titre
Reachability Analysis of Innermost Rewriting
auteur
Thomas Genet, Yann Salmon
article
Rewriting Techniques and Applications 2015, 2015, Warshaw, Poland
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01194530/file/GenetSalmon-RTA15.pdf BibTex

Reports

titre
A Short SPAN+AVISPA Tutorial
auteur
Thomas Genet
article
[Research Report] IRISA. 2015
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01213074/file/main.pdf BibTex

2014

Conference papers

titre
Towards Static Analysis of Functional Programs Using Tree Automata Completion
auteur
Thomas Genet
article
Workshop on Rewriting Logic and its Applications, Santiago Escobar, Apr 2014, Grenoble, France. pp.147 - 161, ⟨10.1007/978-3-319-12904-4_8⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01089993/file/Genet-WRLA14.pdf BibTex

Reports

titre
A Note on the Precision of the Tree Automata Completion
auteur
Thomas Genet
article
[Research Report] IRISA. 2014, pp.13
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01091393/file/Notes.pdf BibTex

2013

Conference papers

titre
Tree Regular Model Checking for Lattice-Based Automata
auteur
Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat
article
CIAA - 18th International Conference on Implementation and Application of Automata, Jul 2013, Halifax, Canada
Accès au bibtex
BibTex
titre
A completion algorithm for lattice tree automata
auteur
Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat
article
CIAA 2013 - 18th International Conference on Implementation and Application of Automata, Jul 2013, Halifax, NS, Canada. pp.134-145, ⟨10.1007/978-3-642-39274-0_13⟩
Accès au bibtex
BibTex

Reports

titre
Towards Static Analysis of Functional Programs using Tree Automata Completion
auteur
Thomas Genet
article
[Research Report] 2013, pp.15
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00921814/file/main.pdf BibTex
titre
Reachability Analysis of Innermost Rewriting
auteur
Thomas Genet, Yann Salmon
article
[Research Report] 2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00848260/file/main.pdf BibTex
titre
Tree Automata Completion for Static Analysis of Functional Programs
auteur
Thomas Genet, Yann Salmon
article
2013
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00780124/file/main.pdf BibTex

2012

Conference papers

titre
Equational Abstraction Refinement for Certified Tree Regular Model Checking
auteur
Yohan Boichut, Benoit Boyer, Thomas Genet, Axel Legay
article
ICFEM, Nov 2012, Kyoto, Japan. pp.299-315
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00759149/file/BoichutBGL-ICFEM12.pdf BibTex
titre
Proving Reachability Properties on Term Rewriting Systems with Strategies
auteur
Thomas Genet, Yann Salmon
article
Workshop on Strategies in Rewriting, Proving and Programming, 2012, London, United Kingdom
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01111038/file/GenetSalmon-IWS12.pdf BibTex

Reports

titre
Tree Regular Model Checking for Lattice-Based Automata
auteur
Thomas Genet, Tristan Le Gall, Axel Legay, Valérie Murat
article
[Technical Report] RT-0424, INRIA. 2012, pp.33
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00687310/file/mainTechRep.pdf BibTex

Preprints, Working Papers, ...

titre
Proofs as Cryptography: a new interpretation of the Curry-Howard isomorphism for software certificates
auteur
Amrit Kumar, Pierre-Alain Fouque, Thomas Genet, Mehdi Tibouchi
article
2012
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00715726/file/RapportHal.pdf BibTex

2010

Journal articles

titre
Equational Approximations for Tree Automata Completion
auteur
Thomas Genet, Vlad Rusu
article
Journal of Symbolic Computation, Elsevier, 2010, 45(5):574-597, May 2010 (5), pp.574-597
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00495405/file/genet-rusu-JSC-SCSS.pdf BibTex

Reports

titre
Equational Abstraction Refinement for Certified Tree Regular Model Checking
auteur
Yohan Boichut, Benoît Boyer, Thomas Genet, Axel Legay
article
[Technical Report] 2010
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00501487/file/rapportHal.pdf BibTex

2009

Conference papers

titre
On the Unobservability of a Trust Relation in Mobile Ad Hoc Networks
auteur
Olivier Heen, Gilles Guette, Thomas Genet
article
Information Security Theory and Practice. Smart Devices, Pervasive Systems, and Ubiquitous Networks, 2009, Belgium. pp.1-11
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00780724/file/wistp2009-1.pdf BibTex
titre
Verifying Temporal Regular properties of Abstractions of Term Rewriting Systems
auteur
Benoît Boyer, Thomas Genet
article
RULE'09, 2009, France. pp.99-108
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00780491/file/main2.pdf BibTex

Habilitation à diriger des recherches

titre
Reachability analysis of rewriting for software verification
auteur
Thomas Genet
article
Software Engineering [cs.SE]. Université Rennes 1, 2009
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00477013/file/Final.pdf BibTex

2008

Journal articles

titre
Le protocole cryptographique de paiement par carte bancaire
auteur
Thomas Genet
article
Interstices, INRIA, 2008
Accès au bibtex
BibTex

Conference papers

titre
Towards an Efficient Implementation of Tree Automata Completion
auteur
Emilie Balland, Yohan Boichut, Thomas Genet, Pierre-Etienne Moreau
article
12th International Conference on Algebraic Methodology and Software Technology - AMAST'08, Jul 2008, Urbana, Illinois, United States. pp.67-82
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00304010/file/finalversion.pdf BibTex

Reports

titre
Certifying a Tree Automata Completion Checker
auteur
Benoît Boyer, Thomas Genet, Thomas Jensen
article
[Research Report] RR-6462, INRIA. 2008, pp.26
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00258275/file/report.pdf BibTex

2007

Conference papers

titre
Using Animation to Improve Formal Specifications of Security Protocols
auteur
Yohan Boichut, Thomas Genet, Olivier Heen, Yann Glouche
article
The 2nd National Conference on Security in Network Architectures and Information Systems, 2007, France
Accès au bibtex
BibTex
titre
Rewriting Approximations for Fast Prototyping of Static Analyzers
auteur
Yohan Boichut, Thomas Genet, Thomas P. Jensen, Luka Le Roux
article
Rewriting Techniques and Applications, 2007, France. pp.48-62
Accès au bibtex
BibTex

2006

Conference papers

titre
Feasible Trace Reconstruction for Rewriting Approximations
auteur
Yohan Boichut, Thomas Genet
article
RTA'2006, Aug 2006, Seattle, United States. pp.123-135
Accès au bibtex
BibTex

Reports

titre
Rewriting for Fast Prototyping of Static Analyzers
auteur
Yohan Boichut, Thomas Genet, Thomas Jensen, Luka Leroux
article
[Research Report] RR-5997, INRIA. 2006, pp.20
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00106330/file/RR-5997.pdf BibTex

2003

Reports

titre
Reachability Analysis over Term Rewriting Systems
auteur
Guillaume Feuillade, Thomas Genet, Valérie Viet Triem Tong
article
[Research Report] RR-4970, INRIA. 2003
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00071609/file/RR-4970.pdf BibTex

2002

Reports

titre
Proving Negative Conjectures on Equational Theories using Induction and Abstract Interpretation
auteur
Thomas Genet, Valérie Viet Triem Tong
article
[Research Report] RR-4576, INRIA. 2002
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072012/file/RR-4576.pdf BibTex

2001

Reports

titre
Reachability Analysis of Term Rewriting Systems with Timbuk
auteur
Thomas Genet, Valérie Viet Triem Tong
article
[Research Report] RR-4266, INRIA. 2001
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072321/file/RR-4266.pdf BibTex

2000

Reports

titre
Rewriting for Cryptographic Protocol Verification - Extended Version
auteur
Thomas Genet, Francis Klay
article
[Research Report] RR-3921, INRIA. 2000
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00072731/file/RR-3921.pdf BibTex

1999

Reports

titre
Induction for Termination
auteur
Isabelle Gnaedig, Hélène Kirchner, Thomas Genet
article
[Intern report] 99-R-338 || gnaedig99a, 1999, pp.21
Accès au bibtex
BibTex

1998

Conference papers

titre
Decidable Approximations of Sets of Descendants and Sets of Normal forms
auteur
Thomas Genet
article
9th Conference on Rewriting Techniques and Applications, 1998, Tsukuba, Japan, pp.151-165
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00098700/file/98-R-137.pdf BibTex

Theses

titre
Contraintes d'ordre et automates d'arbres pour les preuves de terminaison
auteur
Thomas Genet
article
Informatique [cs]. Université Henri Poincaré - Nancy 1, 1998. Français. ⟨NNT : 1998NAN10245⟩
Accès au texte intégral et bibtex
https://hal.univ-lorraine.fr/tel-01747412/file/SCD_T_1998_0245_GENET.pdf BibTex

1997

Reports

titre
Termination Proofs Using gpo Ordering Constraints : Extended Version
auteur
Thomas Genet, Isabelle Gnaedig
article
[Research Report] RR-3087, INRIA. 1997, pp.37
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073604/file/RR-3087.pdf BibTex
titre
Decidable Approximations of Sets of Descendants and Sets of Normal Forms - extended version
auteur
Thomas Genet
article
[Research Report] RR-3325, INRIA. 1997, pp.28
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00073364/file/RR-3325.pdf BibTex