Du Lustre aux jolies leds

Au laboratoire Verimag, nous aidons les ingénieurs informaticiens à prouver automatiquement que leurs programmes sont corrects. Cela est particulièrement important pour les programmes embarqués

Au laboratoire Verimag, les scientifiques cherchent à aider les ingénieurs à prouver automatiquement que leurs programmes sont corrects.

Pour certains programmes, cette question est cruciale, car des vies sont en jeu, notamment quand il s’agit de systèmes embarqués (dans des avions, des trains, des voitures), mais elle est aussi difficile à cause de l'explosion combinatoire.

Une illustration de ce phénomène est donnée par l'échiquier de Sissa, sur lequel le nombre de grains de riz est doublé à chaque case: 1 grain sur la première case 1, 2 grains sur la suivante, puis 4, 8, 16, etc. Un tel échiquier comporte 2^64-1 grains de riz, c'est à dire plus de 18 milliards de milliards de grains, soit l'équivalent de 1000 ans de production mondiale de riz actuellement. Or un programme utilisant 64 cases (ou bits) est un petit programme, et vérifier qu'il est correct dans tous les cas de figure peut nécessiter de considérer des milliards de milliards de cas.

Au laboratoire Verimag, les axes de recherche visant à vérifier la correction de programmes critiques concernent la conception de langages de programmation, ainsi que des méthodes et des outils de preuve et de test automatisé.

Pour illustrer ces travaux, les chercheurs montreront comment vérifier la correction d'un petit programme embarqué sur une carte Arduino, comportant 2 entrées, actionnées par un bouton rouge et un bouton bleu, et 5 sorties, contrôlant l'allumage de 5 leds.

L'intégrité de ce système embarqué sera considérée comme compromise si une séquence d'entrée permet d'allumer les 5 leds simultanément. Le public pourra essayer de déterminer si différents programmes embarqués sur ce système sont dangereux (bogués), comme autant de petits puzzles.

Type d'animation : [Evènement ponctuel] Atelier
Thématiques : Sciences exactes (maths, physique, chimie),Sciences numériques
Publics concernés : Etudiants (18 - 25 ans),Familles,Actifs,Seniors
Tranche d'âge : 5-105
Dates et horaires : samedi 12 octobre 2019 - 10h00 à 18h00
Inscription nécessaire : Non
Lieu : Nuances de sciences : le village du Campus !
Adresse : Bâtiment IMAG, 700 avenue Centrale, 38400 Saint Martin d'Hères
Ville : Saint-Martin-d'Hères (Isère, Auvergne-Rhône-Alpes)
Description du lieu : Grâce à plus de nombreux ateliers, les chercheurs manipulent sous vos yeux et vous font expérimenter les phénomènes scientifiques qu’ils côtoient chaque jour dans leurs labos
Accès : réservations pour les groupes : helene.deschamps@univ-grenoble-alpes.fr
Organisateur : Verimag
Animateurs : Erwan Jahier, Benjamin Wack
Mots clés : Conception sûre de systèmes réactifs/embarqués/critiques,conception de langages,preuve automatique de programmes,#NDS2019