13:00
14:00

[MTV] Thibault Hilaire - A State-of-the-Art Karp-Miller Algorithm Certified in Coq

Petri nets constitute a well-studied model to verify and study concurrent
systems, among others, and computing the coverability set is one of the most
fundamental problems about Petri nets.
Using the proof assistant Coq, we certified the correctness and
termination of the MinCov algorithm by Finkel, Haddad, and Khmelnitsky
(FOSSACS 2020). This algorithm is the most recent algorithm in the literature
that computes the minimal basis of the coverability set, a problem known to be
prone to subtle bugs.
Apart from the intrinsic interest of a computer-checked proof, our certification
provides new insights on the MinCov algorithm. In particular, we
introduce as an intermediate algorithm a small-step variant of MinCov
of independent interest.

salle 178, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159