Approches Formelles dans l'Assistance au Développement de Logiciels

  • Soumission de résumé : 7/02/2014  21/02/2014
  • Soumission article complet : 14/02/2014 28/02/2014
  • Notification aux auteurs : 14/04/2014
  • Soumission version finale : 28/04/2014
CEDRIC
CNAM
ENSIIE
LACL
UPEC
GDR GPL


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

Paris, France, 11-12 Juin 2014