Depuis ces dernières années, les systèmes concurrents sont de plus en plus présents dans nos systèmes informatiques modernes et en particulier dans des systèmes critiques.
Cependant vérifier qu’ils aient un bon comportement n’est pas une chose facile. C’est pour cela que dans cette thèse nous nous intéressons à la vérification formelle, et plus précisément au model-checking. Les réseaux de Petri constituent un modèle bien étudié et bien connu pour vérifier les systèmes concurrents. Le calcul de l’ensemble de couverture est l’un des problèmes les plus fondamentaux concernant les réseaux de Petri, et c’est celui qui nous intéresse dans le cadre de cette thèse. Cependant certains comportements dans les algorithmes calculant l’ensemble de couverture peuvent donner lieu à des bogues subtils et difficiles à trouver. C’est pour cela que nous nous sommes penchés sur les assistants de preuves et plus notamment sur Coq. En l’utilisant, nous avons certifié la correction et la terminaison de l’algorithme MinCov de Finkel, Haddad et Khmelnitsky (FOSSACS 2020). Cet algorithme est l’algorithme le plus récent dans la littérature qui calcule la base minimale de l’ensemble de couverture. Outre l’intérêt intrinsèque d’une preuve vérifiée par ordinateur, notre certification introduit AbstractMinCov, une variante à petits pas de MinCov. L’introduction de ce nouvel algorithme ouvre la voie sur une meilleure compréhension du problème général ainsi que des possibilités pour de futures optimisations.