Model-checking appuyé par des sur et sous-approximations

15 janvier 2024

Yann Thierry-Mieg (LIP6)

L’exposé sera centré sur du model-checking (accessibilité et LTL), avec des stratégies qui mixent des sur-approximations (basées sur SMT) des sous approximations (comme des explorations aléatoires ou dirigée) et des abstractions précises vis à vis de la propriété (comme des réductions structurelles). L’implantation de ces stratégies concrètement pour la vérification de réseaux de Petri permettent à l’outil ITS-Tools de remporter la compétition de model-checking MCC.