Prix Turing 2008

Le communiqué complet de l'ACM :

ICI

Dires de Prix Turing pour étudiants en informatique du XXIe siècle

- " You just read the manual and got the list of instructions and that was all you knew about programming. Everybody had to figure out how to accomplish something and there were of course a zillion different ways of doing it and people would do it in a zillion different ways." J. Backus, (Prix Turing, Fortran) années 40

- "I considered an intelligent thing as a finite automaton connected to an environment that was a finite automaton. I made an appointment to see John von Neumann. He was encouraging. He said, "Write it up, write it up" "
J. McCarthy (Prix Turing, Lisp)

- "To put it simply, the frame problem is not having to mention all the things that don't change when a particular action occurs."
J. McCarthy (Prix Turing, Lisp)

- "All understanding begins with our not accepting the world as it appears." Alan C. Kay (Prix Turing, Smalltalk)

- " By the time I got to school, I had already read a couple of hundred books." Alan C. Kay (Prix Turing, Smalltalk)

- "Computer programming is a bit like a Gregorian chant - a one-line melody changing state within larger scale sections. Parallel programming is more like polyphony." Alan C. Kay (Prix Turing, Smalltalk)

- "They (Air Force) needed programmers. This was back in the days when programming was a low status profession and most of the programmers were women. My boss was a women. They also were taking linguists ... It was actually a pretty interesting bunch." Alan C. Kay (Prix Turing, Smalltalk)

- "People rarely want what they need. Their wants are there for one reason and their needs for another. It is important for technology to match up needs and wants. " Alan C. Kay (Prix Turing, Smalltalk)

- "The mathematical culture of the day was very much identified with the continuum and infinity. Could a finite discrete problem be of any interest ?" E. Dijkstra (Prix Turing)

- "The programmers didn't like the idea at all because it deprived them of the intellectual excitement of not quite understanding what they were doing. They like the challenge of chasing the bugs." E. Dijkstra (Prix Turing)

- "Americans have a pathological fear of formal manipulation. It seems that the United States have a century of demathematicisation which of course is very tragic because in the same century the mathematical computer is invented which is a major mathematical challenge." E. Dijkstra (Prix Turing)

- " [...] This is not a random process. We are not tossing a coin. But is is nondeterministic because you have choices as to the next state (i.e., menu item selection) that you move into. [...] I must say we didn't see all the implications of this. Our notion of nondeterminism was for us a mathematical creation." " M.O Rabin (Prix Turing)

- "We remember thing by structure" M.O Rabin (Prix Turing)

- "Mathematics is the science of patterns. Music is patterns. Computer science does a lot with abstract things and making patterns. Computer science, I think, differs from other fields most in that it constantly jumps levels - from looking at something in the small to looking in the large." D. Knuth (Prix Turing)

- "In general, whatever you're trying to learn, if you can imagine trying to explain it to a computer, then you learn what you don't know about the subject. It helps you ask the right questions. It's the ultimate test of what you know." D. Knuth (Prix Turing)

- "The danger is to get into some branch of theory that becomes self-feeding and doesn'tie back into the real world." R. E. Tarjan (Prix Turing)

Extraits de Out of their minds, Dennis Shasha, Cathy Lazere, Copernicus, Springer-Verlag ISBN 0 487 97992 1

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."