BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:f4e55bc1-b0d7-4bb8-852e-8b458f96a68f
X-WR-CALNAME:[MTV] Thibault Hilaire - A State-of-the-Art Karp-Miller Algori
 thm Certified in Coq
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20251026T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20231029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20241027T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20230326T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20240331T020000
RDATE:20250330T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:f4e55bc1-b0d7-4bb8-852e-8b458f96a68f
DTSTAMP:20260510T232230Z
CLASS:PUBLIC
DESCRIPTION:Petri nets constitute a well-studied model to verify and study 
 concurrent\nsystems\, among others\, and computing the coverability set is
  one of the most\nfundamental problems about Petri nets.\nUsing the proof 
 assistant Coq\, we certified the correctness and\ntermination of the MinCo
 v algorithm by Finkel\, Haddad\, and Khmelnitsky\n(FOSSACS 2020). This alg
 orithm is the most recent algorithm in the literature\nthat computes the m
 inimal basis of the coverability set\, a problem known to be\nprone to sub
 tle bugs.\nApart from the intrinsic interest of a computer-checked proof\,
  our certification\nprovides new insights on the MinCov algorithm. In part
 icular\, we\nintroduce as an intermediate algorithm a small-step variant o
 f MinCov\nof independent interest.
DTSTART;TZID=Europe/Paris:20240314T130000
DTEND;TZID=Europe/Paris:20240314T140000
LOCATION:salle 178\, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159
SEQUENCE:0
SUMMARY:[MTV] Thibault Hilaire - A State-of-the-Art Karp-Miller Algorithm C
 ertified in Coq
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
