Laboratoire I3S - UMR7271

  h
France Deutch English Italiano Spanish
Se connecter

Réservation de salles - Salle 007 (salle de conférence - visioconf niv0 - Algorithmes)(70 personnes max.)
Semaine : lundi 04 juin - dimanche 10 juin

Heurelundi 04 juin mardi 05 juin mercredi 06 juin jeudi 07 juin vendredi 08 juin samedi 09 juin dimanche 10 juin
08:00 - 08:30 Auditions EDSTIC
08:00 à 19:30Allocations UCA
08:30 - 09:00 Allocations UCA ED-STIC
08:30 à 11:30
09:00 - 09:30
09:30 - 10:00
10:00 - 10:30
10:30 - 11:00 Visio Allibert
10:30 à 12:30
11:00 - 11:30
11:30 - 12:00
12:00 - 12:30
12:30 - 13:00 Visio - DAUVIGNAC (LEAT)
12:30 à 17:30
13:00 - 13:30 Répétition oraux stagiaires
13:00 à 16:00		 Présentation Valentin Montmirail
13:00 à 18:00Titre : RECAR: Recursive Explore and Check Abstraction Refinement Résumé : L'approche Counter-Example Guided Abstraction Refinement (CEGAR) a été un grand succès dans la vérification de modèle. Depuis lors, elle a été appliquée à de nombreux problèmes différents. Il s'avère qu'il s'agit d'une approche pratique très efficace pour résoudre le problème QBF qui est PSPACE-complet. Dans ce talk, je vous présenterai une nouvelle approche semblable à CEGAR pour aborder des problèmes PSPACE, approche que nous appelons RECAR (Recursive Explore and Check Abstraction Refinement). Je parlerai ensuite d'une instantiation du framework RECAR pour résoudre le problème de satisfiabilité en logique modale K (problème canonique PSPACE-complet). Nous avons implémentés les deux approches CEGAR et RECAR pour déterminer la cohérence d’une formule en logique modale K au sein du solveur MoSaiC. Nous avons comparé expérimentalement ces approches face aux solveurs de l'état de l’art. L'approche RECAR surpasse l'approche CEGAR sur ces problèmes et se compare favorablement aux solveurs de l'état de l'art sur les benchmarks considérés.
13:30 - 14:00
14:00 - 14:30
14:30 - 15:00
15:00 - 15:30
15:30 - 16:00
16:00 - 16:30
16:30 - 17:00
17:00 - 17:30
17:30 - 18:00
18:00 - 18:30
18:30 - 19:00
^ Haut de la page