Contents

La s\^uret\'e des logiciels

La sûreté des systèmes programmés
Eric Goubault
25 juillet 1999


L'automatisation des processus de production amorcée dès les prémices de la révolution industrielle s'est accélérée depuis l'avènement de l'informatique. En cette fin de siècle, aucun secteur de l'industrie ne pourrait se passer d'ordinateurs qui, aujourd'hui, en calculant des critères de décision, savent gérer des procédés complexes et s'adapter à un environnement externe. La question primordiale est alors celle de savoir si l'on peut faire confiance à ces machines ainsi qu'à leurs logiciels. La " sûreté des systèmes programmés " vise à répondre à cette question, et plus particulièrement à celle de la validité de la composante logicielle.
En 1944, le projet Whirlwind (Massachussetts Institute of Technology) était un système programmé ayant pour but le contrôle du trafic aérien, certes, uniquement militaire. Ces circuits logiques étaient constitués d'une myriade de tubes à vide qui calculaient des fonctions logiques, contrôlées par programme. Quelques satisfactions pouvaient raisonnablement être tirées de cette expérience, si ce n'est que la durée de vie limitée des tubes causait une erreur fatale toutes les 20 minutes environ. De nos jours, la durée de vie des composants est sans conteste très supérieure à celle-ci ; pour autant, le fonctionnement de ces automates modernes est encore bien capricieux, plus à cause d'erreurs dans la programmation (c'est-à-dire le logiciel) qu'à cause de problèmes dus aux circuits électroniques de l'ordinateur.
Pour mieux s'en convaincre, citons quelques unes des plus spectaculaires et récentes erreurs informatiques (ou " bug "[1]). L'explosion du vol 501 d'Ariane 5 après 40 secondes (un demi milliard de dollars de perte en matériel, et plus grave, risque de décrédibilisation d'un programme de 7 milliards de dollars) était due à un problème de conversion de format de nombre dans le programme contrôlant le système de référence inertiel. Une imprécision numérique dans le calcul d'une horloge interne causa la mort de 28 soldats américains pendant la guerre du Golfe après la défaillance d'un missile antimissile Patriot. Des erreurs de calculs sont encore à l'origine de blessures très graves infligées à 6 personnes entre 1985 et 1987 à la suite de trop fortes doses administrées par l'appareil d'irradiation thérapeutique Therac-25. Plus récemment, qui n'a pas eu les oreilles rebattues du fameux et insaisissable " bug de l'an 2000 " ? Au delà de ces exemples catastrophiques, qui n'a jamais pesté en s'apercevant de la perte de ses précieuses données due au " plantage " impromptu d'un logiciel de bureautique? Fatalité, ou problème intrinsèque à l'informatique, comme semble en attester l'air le plus souvent désabusé, mais nullement révolté, des victimes dudit plantage?
L'informatique peut et doit être fiable, de même que le sont les autres domaines de l'ingénierie (la mécanique, l'électricité etc.). Il s'agit en effet d'un impératif répondant aux enjeux technologiques et économiques de l'informatisation. Ces enjeux sont majeurs comme l'actualité le montre. L'activité que l'on appelle " Sûreté des Systèmes Programmés "[2], représentée au CEA/LETI par un peu moins de 25 personnes, s'occupe précisément d'assurer le bon fonctionnement de systèmes informatiques, et de mettre en place le savoir permettant d'éviter de tels accidents.
Les logiciels critiques
Ce n'est nullement une singularité que le CEA se soit doté d'une telle équipe. Le CEA, rappelons-le, a la charge " de donner la maîtrise de l'atome et de ses applications dans les domaines de la recherche, de l'énergie, de l'industrie, de la santé et de la défense ". Cela implique la maîtrise d'oeuvre et l'intégration de métiers très variés, dont celui qui consiste à écrire des logiciels critiques et des logiciels de simulation pour des réacteurs, mais aussi pour la simulation des armes nucléaires. Par logiciel critique, on entend des logiciels dont les erreurs pourraient mettre en péril la vie des hommes ou avoir des répercussions très graves pour le système qu'ils contrôlent. Les exemples catastrophiques décrits plus haut en font partie.
Originellement, le Système de Protection Intégré Numérique (SPIN) pour les centrales nucléaires de 1300 MW fut le premier système critique informatique (opérationnel en 1982) identifié comme tel au CEA. Son rôle est de suivre en permanence les paramètres physiques du coeur de la centrale, de vérifier que ceux-ci restent dans des valeurs acceptables, et de prendre des mesures appropriées dans le cas contraire. En particulier, si la température du coeur dépasse une certaine valeur, la réaction nucléaire doit être stoppée par la chute de barres autour des crayons de matière fissile.
Il existe bien d'autres systèmes critiques, hors CEA, que nous côtoyons plus souvent que le coeur d'une centrale: dès 1983, avec l'Airbus A310, les commandes de vol de certains avions sont contrôlées par logiciel. D'ailleurs les transports regorgent de tels systèmes. Par exemple le métro VAL (et maintenant METEOR) est une ligne automatique gérée par logiciel. Les voitures haut de gamme comportent des logiciels chargés aussi bien de gérer l'allumage électronique que la fermeture des portes, l'ABS et le déclenchement des airbags.
Par extension, les logiciels de transactions financières ou boursières, bien que non critiques dans le sens originel du terme, deviennent des éléments sensibles[3]. Le secteur des télécommunications, ou celui de la micro-électronique, dans lesquels les pannes peuvent impliquer de sévères sanctions financières[4], recèle de plus en plus de logiciels devant être traité avec le même souci de qualité que les logiciels critiques.
Idéalement, quand les méthodes de programmation et les techniques de validation de logiciel, auxquelles le CEA participe pleinement, seront plus mûres et mieux distribuées, c'est la qualité de tous les logiciels qui bénéficiera des avancées faites dans le logiciel critique. Plus les programmes deviennent complexes, plus les outils logiciels se font indispensables dans la vie quotidienne, et plus les attentes concernant les programmes " sûrs " seront grandes et détermineront la vie des éditeurs de logiciels et des constructeurs informatiques. La " sûreté des systèmes programmés " est un secteur d'avenir, dans lequel le CEA s'est engagé, fort de son expérience dans la maîtrise des secteurs critiques. Certains systèmes critiques que nous avons évoqués ont fait l'objet d'une collaboration ou d'accords commerciaux avec le CEA, lequel a ainsi pu transférer certaines de ses technologies à l'industrie.
Programmation et validation
Pour comprendre les actions menées au CEA concernant la sûreté des systèmes programmés, il nous faut commencer par expliquer brièvement comment les logiciels sont conçus et intégrés.
La construction d'un logiciel
L'informatique s'est développée autour d'aspects très expérimentaux. Trop souvent, la pratique veut que l'on procède par essais successifs : programmation, test en exécutant sur quelques données jugées typiques, puis correction des erreurs et ainsi de suite jusqu'à satisfaction du programmeur, ou épuisement du budget, voire du délai.
Cet état de fait s'est institutionnalisé au travers de modèles de développement rationalisant cette démarche et spécifiant les différentes étapes d'écriture puis de validation du code. On distingue en général les phases suivantes ; la première est une phase de spécification. Cette phase n'est rien d'autre qu'une déclaration d'intention sur ce qui doit être fait par le logiciel, dans quel environnement, et sur le problème à résoudre. L'architecture du logiciel est ensuite définie. Elle comporte le découpage des fonctionnalités à programmer en fonctions plus élémentaires et en " modules " aux interfaces claires, afin de pouvoir diviser le travail au mieux parmi les ingénieurs informaticiens (les développeurs). La définition des différentes tâches est d'abord faite à grands traits, pour en arriver finalement à la conception détaillée, qui spécifie entièrement l'ensemble des fonctions à programmer. Puis, vient le codage proprement dit. Ensuite, ou en cours de codage, on essaie de vérifier le programme, s'appuyant sur ses spécifications. Enfin, le programme final est testé en situation, sur les machines et environnements cibles.
Ce schéma général est notoirement insuffisant pour donner les garanties adéquates dans le cas d'un logiciel critique. Le test par exemple, aussi sérieux soit-il, n'est qu'exceptionnellement exhaustif. La complexité des programmes (de nos jours, des centaines de milliers de lignes de code pour les logiciels critiques, et des millions pour les autres), le nombre gigantesque d'états qu'il faudrait théoriquement tester (des chiffres qui peuvent dépasser le nombre de particules dans l'univers) pour être sûr de leurs comportements en toutes situations, font que même avec les machines puissantes dont nous disposons aujourd'hui, il nous faudrait peut-être quelques millénaires, ou même bien plus encore, pour effectuer ces calculs.
Il serait utopique voire dangereux de penser que seule une petite portion de ces tests, choisie pour décrire l'essentiel des comportements possibles, suffirait à garantir le logiciel. Les " bugs ", au sens d'une exécution erronée, amenant éventuellement à l'arrêt brutal du programme, sont des événements rares mais catastrophiques. Par exemple, le comportement général d'un programme effectuant une division de nombres entiers est assez simple à vérifier ; on peut tirer au hasard presque n'importe quel couple de nombres pour tester l'implémentation de la fonction. Hélas, une seule valeur du dividende (zéro) pose un problème grave à l'exécution, et il faut une certaine chance pour tester cette valeur singulière et s'apercevoir si le cas est traité correctement ou pas.
Des modèles du logiciel
Quoiqu'il en soit, on ne peut traiter du logiciel, critique ou pas, comme d'une boîte noire, dont on verra bien à l'usage si elle remplit son rôle correctement. Aucun ouvrage, aucun pont, aucun bâtiment ne serait construit, et encore moins certifié, sur de tels principes. Que faire alors ?
Un scientifique n'étudierait pas un système physique en se contentant d'énumérer ses configurations. Une seule méthode est disponible en ingénierie qui puisse répondre aux exigences de vérification et de justification des choix effectués. C'est à travers la modélisation mathématique que l'on peut donner des garanties sérieuses de bon fonctionnement. Une formalisation mathématique représente en concentré ce qui peut se passer ; c'est par le raisonnement formel que l'on peut en extraire les propriétés essentielles du système, sans tomber dans la fastidieuse énumération de laquelle aucune compréhension des phénomènes ne peut ressortir.
On pourrait être trompé en pensant que la simulation (sur maquette ou sur ordinateur) ou le calcul d'un ouvrage d'art dans des conditions extrêmes (de vent, de température, etc.) ressemble au test du logiciel dans un cas très particulier. Ce serait oublier deux choses. La première est qu'un tel ouvrage mécanique (un pont, un bâtiment etc.) bénéficie des siècles consacrés à la mécanique des milieux continus, à l'élasticité, à l'étude des matériaux. Dans ces conditions, les " bugs " sont assez bien délimités ; si un pont résiste à des conditions cycloniques, il a toutes chances de résister au climat parisien[5]. La deuxième est que si on peut en général utiliser un coefficient de sécurité (une épaisseur double des piliers de soutènement par exemple) pour améliorer la durée de vie d'une construction, il n'en est pas de même pour un logiciel. Ce n'est certainement pas en doublant la taille du code d'une fonction " critique " que l'on va améliorer, loin s'en faut, la qualité d'un logiciel.
Les mathématiques sous-tendant la vérification des logiciels, ou " sémantique ", sont en fait plus proches de la logique, à qui on attribue d'ailleurs souvent la paternité historique de l'informatique, que des équations aux dérivées partielles. Une seule ligne de programme oubliée, une autre en trop, et c'est toute la cohérence d'un programme qui peut être mise à bas, comme on peut rendre faux un long raisonnement par l'utilisation d'une hypothèse erronée.
Encadré 1: Sémantique de programmes
Un programme est une suite de commandes élémentaires, telles des calculs sur des variables, ou des boucles
de traitement répétant un calcul un nombre quelconque de fois ; le petit programme C[6] suivant :
while (x < 100)
x=x+1 ;
opère une transformation simple sur la valeur de la variable x (qui peut être quelconque avant exécution) : il ajoute un à x jusqu'à ce que x soit supérieur ou égal à cent. La sémantique traduit en termes mathématiques cette formulation faite en langage naturel. Associons à chaque ligne de ce programme une " étiquette ", 0 avant le mot clé while, 1 avant l'incrémentation x=x+1, 2 après et 3 après le point-virgule (en sortie de la boucle while). Nous allons également associer à chaque étiquette une formule logique décrivant les états possibles du programme à cette étiquette, pour toutes les exécutions possibles (c'est à dire quelles que soient les valeurs d'entrée de la variable x). Le programme donné en exemple étant extrêmement simple, un état décrit un ensemble de valeurs que peut prendre la variable x. Par exemple, si l'on choisit une formulation ensembliste, un état en le point de contrôle i (0, 1, 2 ou 3) est un ensemble Xi qui vérifie le système d'équations,

En effet, les valeurs possibles de x en le point 1 sont soit celles que l'on avait en 0 en supposant qu'elles permettent à l'exécution de rentrer dans la boucle, donc x est inférieur à 100, soit celles du point 2 en supposant que l'exécution boucle, donc nous savons également que x est inférieur à 100. Si nous avions écrit la première équation dans le format d'une transformation de prédicats logiques, nous aurions . C'est en particulier ce genre de formulation qui est utilisé dans l'outil CEA " CAVEAT "[7]. La plus petite solution de ce système d'équations donne la sémantique, et comme nous nous y attendons,

Nous avons prouvé que l'exécution, si elle se termine (nécessairement en 3), la valeur de x est toujours supérieure à cent, et en utilisant une sémantique un peu modifiée, on pourrait aisément prouver que ce programme se termine toujours sans erreur. Il va de soit que les équations, ainsi que leurs solutions, sont nettement moins intuitives dans les cas réels.
Des outils nécessaires
C'est seulement une fois la définition mathématique effectuée que l'on peut raisonnablement se poser des questions sur des programmes. Il est possible alors, par exemple, d'aider le développeur à trouver et justifier certains tests. Plusieurs techniques sont disponibles et font l'objet de recherches au CEA (voir encadré 2).
Encadré 2: Quelques projets au LETI/DEIN
* AGATHA analyse des spécifications parallèles de haut niveau et vise à générer automatiquement les tests correspondants.
* CAVEAT est un prouveur de programmes écrits en C, utilisant une sémantique logique des programmes.
* CLAIRE est un atelier de simulation logiciel de systèmes complexes. Il permet de tester des composants et des logiciels sans avoir à concevoir de banc test matériel peu adapté.
* GATeL (" Génération Automatique de Tests Lustre ") est développé en collaboration avec le Laboratoire de Recherches en Informatique de l'Université d'Orsay, et permet d'automatiser la génération de tests pour des programmes écrits dans le formalisme temps réel synchrone Lustre.
* OASIS est un système permettant de bénéficier des bienfaits de l'approche Lustre tout en se débarrassant de certaines contraintes temporelles. Il est envisagé de l'utiliser dans le cadre du développement des nouvelles générations de systèmes de protection.
* TWO est un projet européen auquel le CEA participe, visant à la génération automatique de tests et à l'analyse automatique des erreurs possibles que l'on pourrait rencontrer à l'exécution de programmes écrits en C et C++.
Une première voie est d'utiliser la sémantique du langage pour déterminer, par calcul, les environnements d'exécution (valeurs d'entrée du programme par exemple) permettant d'exhiber certains comportements caractéristiques d'un logiciel. Ces comportements caractéristiques peuvent être, comme c'est le cas dans ce que l'on appelle la génération de test structurel, d'atteindre un endroit particulier du programme - un " point de contrôle - ou de suivre un certain chemin, c'est à dire une certaine suite de points de contrôle. Une deuxième est d'utiliser à sa place la spécification du logiciel analysé, elle aussi convenablement formalisée. Les environnements d'exécution ainsi trouvés permettent ensuite de tester le programme. Cette confrontation détermine partiellement si celui-ci se conforme à ses spécifications.
Ces recherches sont, on s'en doute, motivées par les pratiques de développement décrites précédemment. Toutefois, ce n'est pas tout ce que l'on peut faire sur le logiciel. Après tout, le but ultime est de prouver le programme, ou au moins de prouver mathématiquement que certaines " bonnes propriétés "[8] sont toujours satisfaites lors de l'exécution et que des " mauvaises propriétés "[9] n'arriveront jamais. L'idée est de se passer totalement de l'exécution du programme pour ne plus faire appel qu'au raisonnement mathématique pour trouver les erreurs. Un programme est donc conçu dans ce cadre comme une formule de mathématiques[10] qu'il s'agit de prouver. Le problème principal est de savoir comment faire cela intelligemment, car la formule en question fait peut-être un million de lignes !
Il n'y a donc pas d'autre solution que d'automatiser les calculs et les preuves. Le CEA est amené ainsi à développer des outils de vérification automatique. La détermination des tests implique d'utiliser des techniques élaborées telles la résolution de contraintes et la simplification algébrique. La preuve nécessite des technologies et des recherches en démonstration automatique.
Parfois, la preuve complète d'une propriété peut résister au démonstrateur[11]. Il y a alors la possibilité d'approximer (ce que l'on appelle plutôt abstraire) les propriétés et, tout comme les numériciens le font pour simuler des systèmes physiques complexes, de calculer ces approximations par des schémas itératifs. C'est dans les grandes lignes, l'idée de départ de l'interprétation abstraite[12], qui est une des techniques employées au CEA.
Un autre axe de recherche et de développement au CEA concerne la mise au point de systèmes (sur lesquels vont s'exécuter des logiciels), suffisamment contraints pour pouvoir assurer automatiquement certaines bonnes propriétés, en particulier dans le temps réel, mais suffisamment expressifs tout de même pour pouvoir être utiles. Une des particularités des logiciels critiques est que l'on peut se permettre de brider un peu le langage utilisé, ou le système sur lequel ils fonctionneront, pour en supprimer les aspects les plus dangereux, et faciliter ainsi par construction leurs preuves. Cet axe complémentaire se base sur des considérations mathématiques similaires, seules garanties possibles du bon fonctionnement futur des logiciels.
Enfin, une recherche qui n'est pas effectuée au CEA, mais dont les résultats ont été utilisés en particulier dans le monde des transports concerne la synthèse automatique de programmes prouvés, à partir des spécifications formelles. L'idée (celle de la méthode B entre autres) consiste à donner une définition purement logique de ce qu'un programme doit effectuer comme calculs et comme tâches, et à en extraire ensuite, par un processus de raffinement successif, la suite de commandes vérifiant au mieux la spécification. La programmation est ainsi comprise comme un procédé de preuve et d'explicitation d'une spécification logique.
Le rôle du CEA
Le CEA (LETI/DEIN) effectue ces recherches et développements pour assurer le bon fonctionnement, en premier lieu de logiciels critiques. Les équipes y développent la théorie nécessaire, ainsi que les prototypes démontrant leur applicabilité.
En amont, certaines des recherches les plus prospectives sont effectuées en collaboration avec les meilleurs laboratoires universitaires. En aval, des contrats d'études sont passés avec des grands industriels, qui permettent d'une part de faire connaître le savoir faire du CEA et de démarrer le processus de transfert vers l'industrie[13], et d'autre part, de tester les idées et de mieux comprendre les besoins.
Il est naturel que d'autres branches de l'industrie souhaitent bénéficier de l'expérience acquise dans le monde nucléaire, secteur critique s'il en est. Le nombre de contrats passés ces dernières années, avec l'aéronautique et l'industrie automobile notamment, traduit l'intérêt croissant du monde industriel pour la vérification de systèmes informatiques.
En ce qui concerne les logiciels utilisés dans le nucléaire, le CEA met ses outils[14] et son expérience (au travers d'études de cas) à disposition des équipes de vérification de l'Institut de Protection et de Sûreté Nucléaire (IPSN). L'IPSN effectue les contrôles nécessaires, sur demande de la Direction de la Sûreté des Installations Nucléaires (DSIN), qui dépend du Ministère de l'Économie, des Finances et de l'Industrie. En parallèle, l'exploitant des centrales, Électricité de France, rend des comptes à la DSIN et impose des vérifications et des plans d'assurance qualité au constructeur des centrales, FRAMATOME et, en cascade, à tous ses sous-traitants, Schneider-Electric entre autres.
Conclusion et Perspectives
Il est important de comprendre que l'informatique est fondamentalement une activité mathématique. Cela n'étonnera ni le physicien ni l'ingénieur qu'il soit mécanicien, électronicien ou autre. Des siècles de mathématiques ont façonné le langage et clarifié les concepts et méthodes (calcul infinitésimal ou différentiel etc.) utilisés par les ingénieurs et techniciens dans tous les domaines. L'informatique est également une science de l'ingénieur, qui trouve ses fondations dans des théories mathématiques, parfois nouvelles. Pourtant, elle est victime de son succès. Les développements de logiciels sont plus rapides que ne le sont les développements théoriques, seule assise solide pour les méthodes assurant la sûreté des systèmes programmés. Et le travail ne s'arrête pas à la seule théorie. De même qu'il est peu courant de chercher de nouvelles molécules pharmaceutiques et d'en étudier le comportement chimique dans le corps humain en commençant par les équations de la mécanique quantique, il est difficile d'appliquer aveuglément les résultats des théories informatiques. Des techniques sont nécessaires qui permettent de maîtriser la complexité inhérente au domaine. La théorie n'est là essentiellement que pour donner les bons concepts de base (comme par exemple en thermodynamique, la température et la pression). Parmi les développements de la pratique auxquels la théorie et les méthodes de validation du logiciel devront s'adapter prochainement, figureront très certainement les applications distribuées (le " Web " ou les réseaux de calculateurs) ainsi que les programmes de simulation numérique qui posent des problèmes nouveaux de vérification, concernant en particulier la précision de leurs résultats[15]. Le CEA par son implication dans un secteur critique phare, et le LETI en particulier, par sa position de leader dans l'informatique et l'électronique, sont au premier plan dans ce domaine, et se doivent d'y rester.
Encadré 3: Les " bugs " numériques
Un des grands paradoxes de l'informatique est que l'ordinateur est utilisé pour calculer, mais qu'il calcule le plus souvent faux. Les entiers représentables en machine ne correspondent nullement aux entiers mathématiques, ils restent bornés. Les " flottants ", c'est-à-dire les nombres réels informatiques n'ont qu'une lointaine ressemblance avec leurs cousins mathématiques. Par exemple, l'associativité de la multiplication n'est pas valide en général dans les nombres flottants ; de même si une valeur est non nulle, mais très petite, son carré peut être nul  ! Et pourtant la simulation numérique est devenue un outil central de conception et de modélisation en ingénierie. Les numériciens ont bien conscience de ce problème, et il est rare que l'on ne confronte pas la simulation numérique à des expériences grandeur nature. Néanmoins, des erreurs peuvent subsister, bien moins visibles à l'exécution que n'étaient certains des " bugs " catastrophiques érigés en épouvantail au début de cet article ; on peut considérer en effet qu'un calcul trop imprécis voire complètement faux est une erreur de programmation majeure, pouvant amener à des catastrophes. L'exemple du missile Patriot cité dans l'introduction est à cet égard tout à fait symptomatique. Le " bug " était simplement du au fait que l'horloge interne de l'appareil dérivait, car ajoutant dans une mémoire un dixième tous les dixièmes de secondes. Mais un dixième, contrairement à ce que l'on pourrait croire, n'est pas représenté de façon exact sur une machine (binaire) !


[1] " Cafard " en anglais, terme technique consacré depuis qu'un de ces insectes se trouva écrasé par un relais électronique, causant ainsi des problèmes inexplicables sur un ordinateur Mark II pendant la deuxième guerre mondiale. Le lecteur passionné pourra aller admirer ce " bug " au " National Museum of American History of the Smithsonian Institution ".
[2] Elle ne doit pas être confondue avec la sécurité informatique qui est l'activité consistant à éviter l'accès non autorisé à des informations confidentielles.
[3] L'utilisation de l'informatique au coeur des processus industriels est de plus en plus incontournable ; le logiciel peut être adapté sans cesse aux besoins, contrairement à des automates spécialisés. Malheureusement, cette capacité à évoluer augmente les risques de " bugs ", car il est bien difficile de maîtriser l'ensemble d'un logiciel pendant toute sa durée d'utilisation.
[4] On se souvient tous du bug du microprocesseur grand public Pentium, qui aurait semble t-il coûté un milliard de dollars à Intel.
[5] Ici, une simulation peut recouvrir une infinité de conditions possibles " moins dures ". N'oublions pas néanmoins des phénomènes comme la résonance (qui a détruit un pont au milieu du vingtième siècle aux Etats-Unis) ou les phénomènes thermiques cycliques qui fragilisent les matériaux.
[6] C est un langage courant dans le monde industriel qui date des années 70.
[7] Voir encadré 2.
[8] Par exemple, les variables du programme restent toujours dans des valeurs acceptables, ou dans le cas du système de protection des centrales nucléaires, que l'arrêt d'urgence peut toujours se faire lorsque cela devient nécessaire.
[9] Division par zéro, perte des données etc.
[10] Comme les équations de l'encadré 1.
[11] Quelle que soit la technologie utilisée, le problème de la preuve exacte est en général insoluble automatiquement, bien qu'elle soit accessible dans bien des cas.
[12] Introduite à l'origine par P. Cousot (Ecole Normale Supérieure) et R. Cousot (Ecole Polytechnique).
[13] Certains des prototypes sont dans ce cas pris en charge commercialement par des industriels.
[14] Voir l'encadré 2 à propos des différents projets.
[15] Voir l'encadré 3.


Contents