diff --git a/arduino/led_puzzle/doc/puzzle.org b/arduino/led_puzzle/doc/puzzle.org
index 53dd398c54281cfd54f13fc2c799d1e77cdefcd8..b316c07ef249f5ed5c083c6a9a8f56a50f4d6aa8 100644
--- a/arduino/led_puzzle/doc/puzzle.org
+++ b/arduino/led_puzzle/doc/puzzle.org
@@ -11,6 +11,20 @@
 Donnons du Lustre aux leds
 
 
+* laius FDS                                                        :noexport:
+
+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.
+
 * Introduction
  
 Au  laboratoire   =Verimag=,  nous   cherchons  à   aider  les  ingénieurs
@@ -36,7 +50,8 @@ de  problèmes concernent :
 - l'*Analyse   de  programmes*   :   conception  d'algorithmes   (des
   programmes aussi)  qui essaient de *prouver*  qu'un autre programme
   est « *correct* ».
-- l'automatisation des *tests* :  un test qui échoue prouve  qu'un programme n'est *pas* correct.
+- l'automatisation des *tests* : un test qui échoue prouve qu'un
+  programme n'est *pas* correct.
 
 Pour illustrer tous ces axes de recherche, nous allons vous montrer  :
 1. quelques exemples de programmes écrit en Lustre, un langage inventé
@@ -48,8 +63,9 @@ Pour illustrer tous ces axes de recherche, nous allons vous montrer  :
 4. comment tester automatiquement ces programmes.
 
 Il s'agit donc de valider un petit système, composé d'un programme
-Lustre et d'une carte =Arduino=, comportant 2 entrées, *contrôllées*
-par un bouton rouge et un bouton bleu, et *actionnant* 5 leds.
+Lustre et d'une carte =Arduino=, comportant 2 entrées, *actionnées*
+par un bouton rouge et un bouton bleu, et *contrôlant* l'allumage de 5
+leds.
 
 #+BEGIN_CENTER
 \includegraphics[width=.4\linewidth]{arduino.jpg}