Programme

Mercredi 11 Juin

11h 13h : Modélisation – vérification

William Durand, Sébastien Salva. Inférence de modèles dirigée par la logique métier (article long)
Linda Mohand Oussaïd, Ait Sadoune, Yamine Ait Ameur, Mohamed Ahmed Nacer. Modélisation formelle d’IHM multi-modales en sortie avec B Événementiel (article long)
Thomas Polacsek. Réflexions sur les liens possibles entre Argumentation et V&V pour le Logiciel (article court)
Francisca Losavio, Oscar Ordaz, Nicole Levy. Refactoring Graph for Reference Architecture Design Process (article court)

14h 15h30 : Outils formels

Emmanuelle Gallet, Matthieu Manceny, Pascale Le Gall, Paolo Ballarini. Adapting LTL model checking for inferring biological parameters (article long)
David Delahaye, Claude Marché, David Mentré. Le projet BWare : une plate-forme pour la vérification automatique d'obligations de preuve B (article court)
Frédéric Loulergue, Simon Robillard, Julien Tesson, Joeffrey Légaux, Zhenjiang Hu. Dérivation formelle et extraction d'un programme data-parallèle pour le problème des valeurs inférieures les plus proches (article court)
Frédéric Dadeau, Jacques Julliand, Safouan Taha. A Compositional Automata-based Semantics for Property Patterns (article court)

Jeudi 12 Juin

11h 12h30 : Sécurité

Rahma Ben Ayed, Simon Collart-Dutilleul, Philippe Bon, Yves Ledru, Akram Idani. Modélisation et validation formelle des règles d'exploitation ferroviaire (article long)
Jose Pablo Escobedo, Boutheina Bannour, Pascale Le Gall, Juan Gabriel Pedroza Bernal, Christophe Gaston. Designing Sequence Diagram Models for Robustness to Attacks (article court)
Marie-Laure Potet, Laurent Mounier, Maxime Puys, Louis Dureuil. Lazart: a symbolic approach for evaluating the robustness of secured codes against control flow fault injections (article court)
Samiya Hamadouche, Mohamed Mezghiche, Arnaud Gotlieb, Jean-Louis Lanet. Vers une approche de construction de virus pour cartes à puce basée sur la résolution de contraintes (article court)

14h 16h : Systèmes embarqués

Jean-Pierre Jacquot. Premières leçons sur la spécification d'un train d'atterrissage en B événementiel (article long)
Frédéric Boniol. Une proposition pour l'ajout de dimensions dans la programmation de logiciels embarqués (article long)
Fatma Jebali, Mouna Tka Mnad, Christophe Deleuze, Frédéric Lang, Radu Mateescu, Ioannis Parissis. Modélisation et validation formelle de systèmes globalement asynchrones et localement synchrones (article court)
Pascal Manoury, Philippe Baufreton, Jean-Louis Dufour, Etienne Prun, Emmanuel Chailloux, Grégoire Henry, Florian Thibord, Philippe Wang, Etienne Millon. Certification de l'assemblage de composants (article court)

16h30 18h : Test

Sébastien Bardin, Nikolai Kosmatov, François Cheynier. Exécution symbolique et critères de test avancés (article court)
Arnaud Gotlieb, Dusica Marijan. Flower : réduction optimale de suites de test en utilisant la programmation par contraintes (article court)
Aymerick Savary, Mathieu Lassale, Jean-Louis Lanet, Marc Frappier. Formula Negator, Outil de négation de formule (article court)
Guillaume Petiot, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand. Comment la génération de tests facilite la spécification et la vérification déductive des programmes dans Frama-C (article court)

Article long : 30 mn de présentation, article court : 20 mn de présentation

2014