ENS de Cachan
Département
Informatique
Conférences de rentrée 2007









Sylvain Boulmé

Développement de programmes corrects à l'aide de vérificateurs de théorèmes.

Chacun d'entre nous a déjà été confronté à un programme informatique qui ne se comporte pas comme qu'il serait censé le faire. On parle alors d'un programme "bogué". Dans cet exposé, je présenterai certaines méthodes pour construire des programmes "corrects", c'est-à-dire avec une grande garantie d'absence de bogue. Dans ces méthodes, le programmeur démontre (au même sens qu'on démontre un théorème) que son programme fait ce qu'il doit faire, en comparant le source et la spécification du programme. La correction de cette démonstration est elle-même vérifiée par un programme appelé "vérificateur de théorème". Bien sûr, la garantie ainsi obtenue est relative: il faut que "ce que doit faire le programme" ait été correctement formalisé (correction de la spécification), et il faut que les raisonnements formels sur le source du programme soient cohérents avec les exécutions du programme (correction du vérificateur de démonstration, du compilateur et de la plate-forme d'exécution).

Je discuterai de ces aspects méthodologiques dans l'introduction de l'exposé. Ensuite, dans une première partie, je présenterai la "théorie des types" et son incarnation dans le programme "Coq". Cette théorie a révolutionné la notion de démonstration élaborée au début du 20-ème siècle, en formalisant le rapport entre "calcul" (ce qui peut être effectué de manière complètement automatique par un ordinateur) et "déduction" (le raisonnement imparfaitement automatisable). Du coup, bien que cette théorie soit peu compatible avec les fondements classiques des mathématiques (la théorie des ensembles), les outils qui en dérivent semblent adaptés pour vérifier les preuves longues et comportant de nombreux calculs (comme le théorème des 4 couleurs qui a été complètement vérifié en Coq). Autrement dit, ces outils permettent de vérifier des preuves trop longues et/ou trop calculatoires pour être vérifiées par des mathématiciens. Typiquement, les preuves de programmes rentrent dans cette catégorie. Ainsi, plusieurs programmes non-triviaux ont été prouvés en Coq: des programmes de calcul scientifique, un compilateur C-- pour PowerPC (C-- est un sous-ensemble du C utilisé comme langage cible par des compilateurs de langages de plus haut-niveau) et un vérificateur de preuve Coq.

Ceci dit, la notion de calcul en Coq est très élémentaire: elle ne décrit que des "programmes purement fonctionnels", c'est-à-dire des fonctions totales qui ne gèrent pas explicitement la mémoire, et sans interaction avec l'environnement. Dans une deuxième partie, je présenterai donc des "logiques de programmes" (logique de Hoare et calcul de raffinement) qui permettent de raisonner sur des "programmes impératifs" qui manipulent explicitement une notion d'état-mémoire. En particulier, je présenterai succinctement la méthode B (fondée sur le calcul du raffinement) qui a notamment permis de prouver une partie du logiciel de contrôle des trains sur la ligne 14 du métro parisien. Je montrerai enfin comment on peut embarquer ces logiques en Coq, ce qui permet d'en formaliser la correction, et/ou de les utiliser pour raisonner en Coq sur des programmes mélangeant programmation impérative et fonctionnelle.

Références:

  • Vulgarisation:
 + Gérard Berry. Le logiciel, objet de notre quotidien.
   Conférence vidéo de l'université de tous les savoirs, 2000.
   http://www.canal-u.com/canalu/affiche_programme.php?vHtml=1&programme_id=254.
 + Gilles Dowek. Les Métamorphoses du calcul. Le Pommier, 2007.
  • Livres scientifiques:
 + J.-R. Abrial. The B-Book. Cambridge University Press, 1996.  
 + R.-J. Back, J. von Wright. Refinement Calculus: A Systematic Introduction. Springer, 1998.
 + Y. Bertot, P. Casteran. Interactive Theorem Proving and Program Development. 
   Coq'Art: The Calculus of Inductive Constructions. Springer, 2004.
 + J.-Y. Girard, Y. Lafont, P. Taylor. Proofs and types. Cambridge University Press, 1989.
 + J.-F. Monin. Comprendre les méthodes formelles. Masson, 1996.
  • Pages Web:
 + Site de Coq:                           http://coq.inria.fr/
 + Why, une logique de Hoare en Coq:      http://why.lri.fr/
 + B, une méthode basée sur le calcul de raffinement:
      http://www-lsr.imag.fr/B/
 + Raffinement d'ordre supérieur en Coq:
      http://www-lsr.imag.fr/users/Sylvain.Boulme/horefinement/

Albert Cohen

100 milliards de transistors, et moi et moi et moi.

La loi de Moore sur semi-conducteurs approche de sa fin. L'evolution de l'architecture de von Neumann à travers les 40 ans d'histoire du microprocesseur a conduit à des circuits d'une insoutenable complexité, à un très faible rendement de calcul par transistor, et à une forte consommation énergétique. Le fossé se creuse entre les capacités brutes des circuits integrés et les performances observables sur des systèmes réels (ordinateurs généralistes, dédiés au calcul, ou enfouis). Ce fossé met en danger l'ensemble de l'édifice socio-technologique reposant sur la croissance exponentielle de la puissance de calcul. Cela se traduit par des défis passionnants pour la recherche en architecture de processeurs, en compilation et en langages de programmation. Nous passerons en revue les fondements et les enjeux de ces recherches, en les illustrant sur des cas réels.

Isabelle Guérin-Lassous

Les réseaux sans fil : architectures du futur, problèmes du futur.

Les réseaux sans fil connaissent un essor indéniable. Après les réseaux cellulaires de type GSM, nous voyons apparaître le WiFi, le Bluetooth, Le WiMax, le ZigBee, etc. Les terminaux multi-technologies sont en train de faire leur apparition sur le marché. Après une description des caractéristiques des réseaux sans fil, je ferai un état de l'art sur les technologies sans fil existantes et émergentes. Nous examinerons ensuite certaines applications potentielles. Enfin, certains problèmes théoriques et algorithmiques soulevés par ces technologies et ces applications seront décrits. Ces descriptions me permettront de terminer le cours sur une revue des problèmes de recherche actuels dans le domaine.

Philippe Flajolet

Algorithmique de grands flux de données: de l'analyse aux programmes.

Diverses applications, des réseaux à  la fouille de données en passant par le traitement de données textuelles, necessitent l'extraction automatique de caractéristiques quantitatives de grands ensembles de données. Par exemple, le calcul de la cardinalité (le nombre d'éléments différents vérifiant divers critères), l'entropie empirique, ou encore les moments de fréquence. Au cours des deux dernières décennies, plusieurs algorithmes ont été proposés qui permettent de traiter des flux de données massifs avec une mémoire très petite (souvent de quelques kilo-octets), tout en fournissant des estimation de bonne qualité (quelques pourcents, typiquement). On montrera quelques uns des principaux algorithmes dont l'analyse, voire même souvent la conception, repose sur diverses méthodes de combinatoire analytique. L'accent sera mis en particulier dans cet exposé sur l'articulation entre problèmes algorithmiques spécifiques, méthodes mathématiques d'analyse d'algorithmes, et conception de programmes performants.

Rémi Gilleron

Modèles d'automates et modèles probabilistes pour les arbres XML, apprentissage et applications

Nous nous plaçons dans le cas classique de l'arité fixée et présentons les automates d'arbres, les automates d'arbres pondérés et les séries rationnelles d'arbres. Nous discutons les extensions de ces modéles au cas des arbres d'arité non bornée où un noeud peut avoir un nombre non borné de fils. Nous considérons ensuite l'apprentissage de deux modèles pour les arbres : les automates stochastiques et les champs de Markov conditionnels. L'exposé sera illustré par la démonstration d'un Web service de génération automatique de flux RSS personnalisé.

Guy Mélançon

Visualisation et exploration interactive de graphes

La masse de données disponibles, hétérogènes et constamment renouvelées, pose un défi de taille dans quantité de domaines: sécurité, veille stratégique et concurrentielle ("intelligence économique"), bio-informatique, etc. Une voie prometteuse est de développer des cartographies interactives permettant à un analyste expert du domaine de fouiller interactivement les données afin de cerner les propriétés qui pourraient s'y trouver. La visualisation d'information vise à développer des cartographies et des dispositifs d'interaction tirant profit des capacités d'analyse du système visuel humain. Cette discipline est née de travaux se plaçant dans le champ de l'infographie, de l'interaction homme-machine, de la psychologie cognitive, de la sémiotique, du design graphique, de la statistique graphique, de la cartographie et des arts graphiques. Les efforts récents de la NSH/NIH et la création de Visualization Center aux Etats-Unis définissent un agenda de travail associant data mining et visualisation pour en faire le "Visual Analytics".

Les graphes apparaissent naturellement dans ce champ de recherche, d'une part parce qu'ils permettent de modéliser aisément les situations à analyser et d'autre part parce qu'ils offrent une vaste littérature mathématique et algorithmique dont on peut tirer profit. C'est sur ce chapitre particulier que portera l'exposé, soulignant à la fois comment on peut utiliser les graphes et les indices structuraux définis sur leur topologie pour avancer dans l'analyse des données étudiées. Il sera aussi question de cartographie interactive et de dessin de graphes. Une attention particulière sera accordée à l'utilisation de hiérarchies de graphes (graphes imbriqués) comme outils d'analyse et de navigation de grands ensembles de données. Les notions présentées dans l'exposé seront abondamment illustrées par des cas d'études, des images et quelques vidéos.

Philippe Cinquin

From Computer Assisted Medical Interventions (CAMI) to Quality Inspired Surgery.

First generation of research and industrial development lead to successful introduction of Information Technology (computers, navigation devices, robots, ) in the Operating Room. It can now be proven that such techniques significantly enhance the clinical outcome of surgical procedures. To go further on this road towards Quality, the challenge now is to "invert this movement": instead of moving the computer in the Operating Room, we should embed the surgeon (or at least his or her expertise) into the IT-based tools he or she uses. Taking up this challenge implies a major renewal of the currently available set of knowledge and expertise. This will replace Quality (in its medical meaning) at the heart of the process of combining surgery and informatics. Models of various types will need to be developed and used to achieve a global vision of the therapeutic process, on the basis of which Quality Inspired Surgery could be designed and performed. We will show how this vision lead to the design of very light robots in several applications (remote ultrasound image acquisition, Light Endoscopic Robot, Light Puncture Robot, Robotized Distraction Device for ligament balance monitoring in Total Knee Arthroplasty, ). We will conclude with perspectives of implantable robots capable of using as a source of energy the glucosis naturally present in the human body.


Contacter le Département Informatique
Dernières modifications : le 10/11/2008