Email Gateway (Jun 16 2026 at 12:20): Email Gateway (Jun 16 2026 at 12:20):From: Sophie Tourret <sophie.tourret@loria.fr>
Dear all,
I have a funded postdoc position for two years, planned to start this
autumn at Inria in Nancy, France. The general topic of the postdoc is
the Isabelle/HOL formalization of the cryptographic protocol verifier
ProVerif ( https://bblanche.gitlabpages.inria.fr/proverif/ ).
The details of the offer are available here:
https://recrutement.inria.fr/public/classic/en/offres/2026-10141 .
If you want to know more, don't hesitate to contact me.
Kind regards,
Sophie
--
Sophie Tourret
researcher, Inria, France
senior guest researcher, MPI for Informatics, Germany
Email Gateway (Jun 16 2026 at 13:01):From: Thomas Genet <thomas.genet@irisa.fr>
Bonjour Sophie,
Ah ben ça m'intéresse cette offre de postdoc! ;-)
Bon désolé j'ai plus l'âge...
En fait le sujet m'intéressait à une époque. Avec un doctorant on avait
défini un certificateur de point fixe (pour des automates et systèmes de
réécriture) prouvé en Coq et extrait en OCaml. Ca permettait de prouver
qu'un automate reconnaissait bien un ensemble de termes (non borné)
saturé par un système de réécriture.
Or automate+réécriture ça permet aussi de faire de la vérif de
protocoles crypto.
Je m'étais posé la question de savoir si certifier que l'ensemble de
clauses de Horn produit par Proverif est bien une sur-approximation de
l'ensemble des faits déductibles par les clauses originales serait aussi
"facile" à faire que dans le cas de la réécriture+automates.
Mais j'imagine que dans ton projet de post-doc il y a aussi toute la
partie traduction du Pi-calcul vers clauses de Horn... et là ça va être
moins la fête :-)
A bientôt,
Thomas
Le 16/06/2026 à 11:41, Sophie Tourret a écrit :
Dear all,
I have a funded postdoc position for two years, planned to start this
autumn at Inria in Nancy, France. The general topic of the postdoc is
the Isabelle/HOL formalization of the cryptographic protocol verifier
ProVerif ( https://bblanche.gitlabpages.inria.fr/proverif/ ).The details of the offer are available here: https://
recrutement.inria.fr/public/classic/en/offres/2026-10141 .If you want to know more, don't hesitate to contact me.
Kind regards,
Sophie
--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet@irisa.fr
http://people.irisa.fr/Thomas.Genet
Last updated: Jul 02 2026 at 07:34 UTC