Joseph SIFAKIS, premier prix Turing français

Le français Joseph Sifakis vient d'obtenir
le prix Turing 2007. C'est le
premier français obtenant ce prix, considéré
comme "le Nobel de
l'informatique". Joseph Sifakis est un
spécialiste du "model checking".
Il y a deux approches de la vérification
des logiciels :
- la preuve que nous traitons dans le cadre
de notre enseignement de la méthode B dans
notre module Spec1  en première année d'IUT
- la "vérification de modèles" que nous traitons
dans le cadre de notre module Spec2 en première
 année d'IUT.
(Mais nous NE traitons pas des algorithmes de
"model checking").
Parmi les techniques utilisées en "model checking"
il y a les BDD (ne pas confondre avec les Bases De
Données ou avec les Bases de Données Déductives !)
lire ici
http://www2.cnrs.fr/presse/communique/1280.htm
http://www.acm.org/press-room

Il a obtenu ce prix avec Avec Edmund Clarke
(Carnegie Mellon University, USA)
Allen Emerson (University of Texas, Austin, USA).

Ces deux universités américaines sont bien
connus pour leurs travaux en informatique et ont
déjà eu des Prix Turing.

Les pages web de Joseph Sifakis

Extrait d'une courte présentation de Joseph Sifakis
et Jean-François Monin dans Arago 20
Applications des techniques formelles au logiciel,
Observatoire Français des Techniques Avancées,
Lavoisier, ISBN 2-906028-06-1

"On peut distinguer deux approches principales à
la vérification :

• celle qui met en oeuvre un système d'inférence, i.e. un ensemble bien défini et formalisé de règles de raisonnement issues de la logique (modus ponens, récurrence, substitution de valeurs égales, etc.) ; les outils de support sont des assistants à la preuve (PVS, HOL, Coq, atelier B, LP,...)
• celle qui se fonde sur la construction d'un modèle généralement fini qui représente le système de transition représentant le comportement de l'application modélisée. La vérification des propriétés s'effectue en parcourant exhaustivement ce modèle. Les outils support sont basés sur le principe de l'évaluation des propriétés sur un modèle, connu sous le nom de model checking (MEC, Caesar-Aldebaran, Auto, Spin, Cospan, SMV, ...)

[...] concernant la seconde approche, des techniques de représentation implicite ou symbolique des états permettent de condenser la représentation du modèle. Notons, en particulier, la technique des BDD pour la représentation symbolique des fonctions booléennes, qui trouve des applications intéressantes à la vérification des systèmes à états finis."