BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:badf1b03-db9f-4c4e-9674-8750921618d4
X-WR-CALNAME:[MTV] Nicolas Amat (IRIT) - What is Polyhedral Reduction? ... 
 and how we use it to accelerate the verification of reachability problems.
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20240331T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20211031T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20221030T030000
RDATE:20231029T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20220327T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20230326T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:badf1b03-db9f-4c4e-9674-8750921618d4
DTSTAMP:20260510T232457Z
CLASS:PUBLIC
DESCRIPTION:We define a method that takes advantage of structural reduction
 s to accelerate the verification of reachability problems. We prove the co
 rrectness of this method using a new notion of equivalence between nets th
 at we call polyhedral abstraction. Our approach has been implemented in a 
 tool\, named SMPT\, that provides SMT-based methods. We present an adaptat
 ion of the Property Directed Reachability (PDR) decision procedure that pe
 rmits to generate some certificate of invariance for generalised nets. We 
 also propose a new method for accelerating the computation of the concurre
 ncy relation\, that is all pairs of places in a Petri net that can be mark
 ed together. Our approach relies on the same state-space abstraction\, tha
 t involves a mix between structural reductions and linear algebra\, but th
 is time using a new data-structure that is specifically designed for our t
 ask.
DTSTART;TZID=Europe/Paris:20220707T103000
DTEND;TZID=Europe/Paris:20220707T113000
LOCATION:LaBRI 178 - zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159
SEQUENCE:0
SUMMARY:[MTV] Nicolas Amat (IRIT) - What is Polyhedral Reduction? ... and h
 ow we use it to accelerate the verification of reachability problems.
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
