Axe Spécification et Vérification

Paris 13 > LIPN > LCR > Axe Spécification et Vérification

Thématiques

Voir notre rapport d’activités 2003 − 2006 au sein du LIPN (le rapport 2007−2011 est en cours de rédaction).

Voir la biblio de notre axe de recherche, ou la bibliographie des membres.

Dernière minute

Notre équipe recrute un ingénieur (CDD de 4 mois) et un stagiaire de Master 2, afin d’effectuer l’intégration de plusieurs logiciels à la plate-forme CosyVerif. Recrutement dès que possible (printemps−été 2012). Détails du sujet ici.

Stages 2012

Notre axe de recherche propose une liste de stages pour étudiants de Master, pour la période printemps − été 2012.

Si l’un de nos sujets vous intéresse, merci de contacter le(s) chercheur(s) responsables du sujet. N’hésitez pas non plus à nous contacter pour toute question.

Sujet	Proposé par	Niveau
Approche incrémentale et modulaire pour la vérification de propriétés temporelles linéaires sur les réseaux de Petri [PDF ]	Kaïs Klai et Laure Petrucci	Master 2
Vérification modulaire de systèmes temporisés : aspects structurels et dynamiques [PDF ]	Kaïs Klai et Laure Petrucci	Master 2
Une méthode d’analyse et spécification pour les systèmes complexes avec des réseaux de Petri de haut niveau et des spécifications algébriques [PDF ]	Christine Choppy et Laure Petrucci	Master 2
Modélisation des diagrammes états-transitions UML [PDF ] [PDF ]	Étienne André, Christine Choppy et Kaïs Klai	Master 2
Vérification automatisée des diagrammes états-transitions UML [PDF ] [PDF ]	Étienne André, Christine Choppy et Kaïs Klai	Master 2
Model-checking distribué : algorithmes multi-cœurs efficaces [PDF ] [PDF ]	Sami Evangelista et Laure Petrucci	Master 2
Vérification paramétrée de systèmes temps réel par des réseaux de Petri temporels [PDF ] [PDF ]	Étienne André	Master 2
Model-checking distribué de réseaux de Petri temporels et à priorités [PDF ] [PDF ]	Étienne André, Sami Evangelista et Laure Petrucci	Master 2
Un algorithme incrémental de vérification de propriétés LTL [PDF ] [PDF ]	Kaïs Klai et Laure Petrucci	Master 2

Outils

• Helena : un outil de vérification pour les réseaux de Petri de haut niveau
• IMITATOR : synthèse de paramètres pour automates temporisés (co-développé par le LSV)
• MCsog : model checker LTL\X basé sur les graphes d’observation symboliques
• modsog : outil permettant de construire un graphe d’observation symbolique de façon modulaire

Projets

• CosyVerif : Plate-forme d’intégration des outils du groupe MeFoSyLoMa
• Merlion : Vérification de logiciel de la spécification à l’implémentation
• Neoppod : analyse formelle d’un protocole de bases de données réparties à large échelle

Collaborations et visiteurs

• Jonathan Billington (University of South Australia, Australie)
• Patrice Carle (Onera)
• Philippe Darondeau (IRISA, Rennes, France)
• Jörg Desel (Universität Hagen)
• Jin-Song Dong (National University of Singapore)
• Laurent Fribourg (LSV, Cachan, France)
• Maritta Heisel (Duisburg−Essen)
• Kurt Jensen (Université d’Århus, Danemark)
• Romain Kervarc (Onera)
• Ekkart Kindler (DTU)
• Lars Michael Kristensen (Bergen University College, Bergen, Norvège)
• Charles Lakos (University of Adelaide, Australie)
• Shang-Wei Lin (National University of Singapore)
• Yang Liu (National University of Singapore)
• Gianna Reggio (Université de Gênes, Italie)
• Romain Soulat (LSV, Cachan, France)
• Jun Sun (Singapore University of Technology and Design)

Anciens membres

• Olivier Bertrand (DGA)
• Fabien Bonnefoi
• Samir Youcef (LORIA, Nancy, France)

Séminaires

• MeFoSyLoMa