In recent years, concurrent systems have become an increasingly common feature of modern IT systems, especially mission-critical systems. However, checking that they behave correctly is no easy task. That’s why in this thesis we focus on formal verification, and more specifically on model-checking. Petri nets are a well-studied and well-known model for verifying concurrent systems. The computation of the coverability set is one of the most fundamental problems concerning Petri nets, and it is the one that interests us in this thesis. However, certain behaviors in coverability set computation algorithms can give rise to subtle and hard-to-find bugs. That’s why we’ve turned our attention to proof assistants, and in particular to Coq. Using it, we certified the correction and termination of the MinCov algorithm by Finkel, Haddad and Khmelnitsky (FOSSACS 2020). This algorithm is the most recent in the literature to calculate the minimum basis of the coverability set.
In addition to the intrinsic interest of a computer-verified proof, our certification provides AbstractMinCov, a small-step variant of MinCov. The introduction of this new algorithm opens the way to a better understanding of the general problem, as well as possibilities for future optimizations.