Karoliina Lehtinen, aux racines de la vérification de programmes
Karoliina Lehtinen, chargée de recherche CNRS au Laboratoire d’informatique et des systèmes (LIS - CNRS/Aix-Marseille Université), travaille sur les fondements théoriques de la vérification de programmes. Elle est récompensée par la médaille de bronze du CNRS.
Les programmes informatiques sont partout. Mais comment s’assurer qu’ils fonctionneront comme prévu ? Karoliina Lehtinen, chargée de recherche au CNRS, travaille sur les fondements théoriques qui rendent possible leur vérification automatique. À l’interface entre logique, automates et théorie des jeux, elle développe des outils conceptuels qui pourraient, à terme, renforcer la fiabilité des logiciels.
C’est pendant ses études qu’elle découvre que certaines propriétés logiques peuvent se traduire en jeux. Ce pont entre logique et stratégie devient par la suite le fil rouge de ses recherches. Après une formation à Cambridge, elle soutient une thèse à Édimbourg sur la complexité du μ-calcul modal, un langage logique central en vérification. Elle y explore une question ouverte depuis plus de quarante ans : est-il possible de simplifier certaines formules pour en accélérer la vérification ? Elle propose pour cela un algorithme capable de détecter des cas simplifiables à certains sous-problèmes de cette question toujours ouverte.
Son parcours post-doctoral, entre l’Allemagne, Israël et l’Angleterre, la mène ensuite vers la théorie des jeux de parité. En 2018, elle publie un algorithme fondé sur ces jeux qui contribue à faire avancer la vérification logique. Elle devient également experte d’un modèle original jusqu’alors peu étudié : les automates déterministes en histoire. Ces automates hybrides, à mi-chemin entre déterminisme et non-déterminisme, offrent un compromis précieux entre expressivité et efficacité. Elle en propose plusieurs variantes, aujourd’hui intégrées à des outils académiques. Elle contribue ainsi fortement à l’émergence de ce domaine désormais florissant.
Depuis son arrivée au CNRS en 2021, elle poursuit ses travaux avec un sens aigu des enjeux fondamentaux. Avec Aditya Prakash, post-doctorant à Aix-Marseille et membre du LIS, elle a récemment résolu une conjecture qui bloquait sa communauté depuis des années. Une réussite qui nourrit sa prochaine ambition : « Je voudrais m’attaquer à une question me suit depuis ma thèse : quelle complexité faut-il pour décrire un langage d’arbres ? Avec les nouveaux outils issus des jeux de parité, nous avons peut-être enfin de quoi avancer », confie-t-elle.