19 au 21 novembre
Lille, IRCICA
Les journées annuelles du GT Vérification 2024 auront lieu du 19 au 21 novembre à Lille, au sein de l’IRCICA. Elles s’étaleront sur 4 demi-journées, du 19 après-midi au 21 matin. Cette année, les journées seront en partie communes avec les journées annuelles du GT SCALP (Structures Formelles pour le Calcul et les Preuves) du GDR IFM, qui auront lieu du 18 au 20. Plus précisément, le 19 après-midi et le 20 matin seront des demi-journées communes, dédiées aux interfaces entre les deux GT.
Les journées du GT-Vérif visent à rassembler la communauté française en vérification formelle, et en particulier les chercheurs juniors, doctorants et post-doctorants, avec pour objectif de favoriser les collaborations, l’ouverture sur des thématiques liées à la vérification, et pourquoi pas préparer de futures visites de doctorant(e)s.
Elles ont pour ambition de couvrir tous les domaines de la vérification formelle, incluant (entre autres !) :
- la vérification informatique de systèmes, modélisant des systèmes de freinage aux protocoles de communications en passant par les programmes,
- l’emploi de techniques de preuve automatiques ou interactives (model-checking, déduction automatique, assistants de preuve, solveurs SMT, etc. ainsi que leurs combinaisons),
- l’utilisation de logiques pour raisonner sur les propriétés des systèmes (par exemple les logiques temporelles, spatiales, probabilistes ou avec données),
- les techniques d’abstraction pour la vérification.
APPEL A EXPOSES / INSCRIPTION
Toute personne souhaitant donner un exposé lors de ces journées est invitée à l’indiquer dans le formulaire d’inscription.
Si vous souhaitez donner un exposé mais n’avez pas encore d’idée précise du sujet, vous pouvez laisser les champs vides, et nous les envoyer plus tard par mail à mailto:copil-gt-verif@inria.fr.
PROGRAMME
Orateurices invité·es :
- David Baelde (ENS Rennes, IRISA) – conjoint avec SCALP
- Julie Cailler (U Lorraine, LORIA) – SCALP
- Arthur Charguéraud (Inria, ICube) – Vérif
- Jean Goubault-Larrecq (ENS Paris-Saclay, LMF) – SCALP
- Mickaël Randour (UMons) – Vérif
- Sylvain Salvati (ULille, CRIStAL) — conjoint avec SCALP
- Lina Ye (CentraleSupélec, LMF) (détails) – Vérif
DATES IMPORTANTES
- Proposition d’un exposé : 10/10
- Date limite d’inscription : 10/10
- Journées : 19 au 21/11
INSCRIPTION
Merci de remplir le formulaire d’inscription.
PROGRAMME COMPLET
Disponible ici
INFORMATIONS PRATIQUES
Disponibles ici
ORGANISATION
- Nathalie Bertrand (Inria, IRISA) – Vérif
- Pierre Clairambault (CNRS, LIS) – SCALP
- Chantal Keller (UP Saclay, LMF) – SCALP
- David Nowak (CNRS, CRIStAL)
- Pierre-Alain Reynier (Aix-Marseille Université, LIS) – Vérif
- Vlad Rusu (Inria, CRIStAL)
- Alexis Saurin (CNRS, IRIF) – SCALP
Détails des exposés
Lina Ye (CentraleSupélec, LMF)
Decisiveness Analysis of Infinite (Dynamic) Probabilistic Models
Decisiveness of infinite Markov chains with respect to some (finite or infinite) target set of states is a key property that allows to compute the reachability probability of this set up to an arbitrary precision. Most of the existing related works assume constant weights for defining the probability of a transition in the considered models. However numerous probabilistic modelings require (dynamic) weights that depend on both the current state and the transition. So we study and demonstrate that in the dynamic settings, the decisiveness is undecidable for both probabilistic one-counter machines and polynomial probabilistic Petri nets. Fortunately, we succeed to identify some interesting subclasses for which either the decisiveness is decidable in polynomial time or the models themselves are decisive with respect to a finite set.