Groupe de travail

Méthodes de Test pour la Vérification et la Validation
MTV2

Réunion MTV2 du 9 décembre 2015 à CentraleSupélec

La prochaine réunion du groupe aura lieu le mercredi 9 décembre 2015 dans les locaux de CentraleSupélec à Châtenay-Malabry.

Cette réunion est soutenue par le GDR GPL.

Pour toute demande ou modification d'inscription tardive (après le 28 novembre 2015), merci d'envoyer un mail aux organisateurs locaux : Pascale Le Gall et Nikolai Kosmatov, en précisant les nom, prénom, institution, téléphone et email des participants.

Venir à CentraleSupélec

La réunion aura lieu sur le campus Châtenay en salle D401 au 4e étage du bâtiment Dumas.

Le plan et les moyens d'accès au site sont donnés à l'adresse : http://www.ecp.fr/plan_d_acces

Par mesure de sécurité, un contrôle de pièces d'identité pourra être effectué à l'entrée du campus.

Programme

La durée des exposés sera de 20 min.+ 5 min. de questions.

9h30-10h : Accueil, café

10h-10h50 : Session 1

  • Adel Djoudi (CEA LIST). BINSEC: A platform for binary code analysis.
  • Imen Boudhiba (CentraleSupélec). Model-based Testing from IOSTS Enriched by Program Calls and Contracts.

Pause

11h20-12h35 : Session 2

  • Mouna Tka (LCIS). Testium : outil de génération automatique de données de test pour les systèmes synchrones.
  • Franck Védrine (CEA LIST). Numerical accuracy analysis directed by dynamic traces.
  • Romain Aissat (LRI). A verified technique for the elimination of infeasible paths in call-graphs.

Déjeuner

14h-15h : Session 3 (in English) - Invited talk

Cristian Cadar. Symbolic Execution for Evolving Software
Abstract: One of the distinguishing characteristics of software systems is that they evolve: new patches are committed to software repositories and new versions are released to users on a continuous basis. Unfortunately, many of these changes bring unexpected bugs that break the stability of the system or affect its security. In this talk, I describe our work on devising novel symbolic execution techniques for increasing the confidence in evolving software: a technique for reasoning about the correctness of optimisations, in particular those that take advantage of SIMD and GPGPU capabilities; a technique for high-coverage patch testing, and a technique for revealing regression bugs and behavioural divergences across versions.
Bio: Cristian Cadar leads the Software Reliability Group in the Department of Computing at Imperial College London. His research interests span the areas of software engineering, computer systems and security, with an emphasis on designing practical techniques for improving the reliability and security of software systems. Cristian received a PhD in Computer Science from Stanford University, and undergraduate and Master's degrees from the Massachusetts Institute of Technology. He was awarded the Jochen Liedtke Young Researcher Award in 2015, an EPSRC Early-Career Fellowship in 2013, and artifact or paper awards at ISSTA 2014, ESEC/FSE 2013 and OSDI 2008.

Pause

15h15-16h55 : Session 4 (in English):

  • Jean-Marie Mottu (LINA). Discovering Model Transformation Pre-conditions using Automatically Generated Test Models.
  • Thierry Jéron (IRISA). Enforcement of timed properties.
  • Burkhart Wolff (LRI). Testing the IPC Protocol for a Real-Time Operating System.
  • Julien Signoles (CEA LIST). Fast as a Shadow, Expressive as a Tree: Hybrid Memory Monitoring for C.

17h - Annonces : journées du GDR 2016, suite du groupe de travail.