Collège de France (Sciences et technologies)

Collège de France (Sciences et technologies)

France

Collège de France (Sciences et technologies)

Episodes

06 - Prouver les programmes : pourquoi, quand, comment ? - PDF  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Sixième leçon : Vérification et optimisation booléennes d'automates et circuits Ce dernier cours de 2014-2015 introduit les méthodes implicites de manipulation de systèmes de transitions, à travers les méthodes de calcul booléen utilisées à la fois pour la vérification formelles et pour l’optimisation de circuits électroniques et de programmes qui peuvent se réduire au calcul booléen. Ces méthodes ont révolutionné le domaine en permettant des vérifications formelles de systèmes dont le calcul explicite des états et transitions est impossible, car la taille des formules manipulées par les méthodes implicites est largement indépendante de celle des systèmes qu’ils décrivent. Nous expliquons d’abord les codages booléens d’ensembles, de relations et de fonctions, et montrons comment calculer l’image directe et l’image inverse de sous-ensembles par des fonctions. Nous étudions ensuite les codages booléens d’automates déterministes et non-déterministes, ainsi que leurs implémentations en circuits électroniques. Nous rappelons le fait que le circuit canoniquement associé à un automate non-déterministe est lui déterministe comme tous les circuits combinatoirement acycliques, ce qui montre clairement que le qualificatif « non-déterminisme » est particulièrement mal choisi : en vérification booléenne comme en optimisation de circuits, il est inutile de déterminiser les automates, et c’est souvent nuisible à cause de l’explosion exponentielle que la déterminisation peut produire. Nous montrons comment la vérification formelle de propriétés de sûreté définies par des observateurs se réduit au calcul des états accessibles, et comment effectuer ce calcul de manière implicite. Nous introduisons la première structure fondamentale du calcul booléen, les Binary Decision Diagrams, développés par R. Bryant au milieu des années 1980 (et indépendamment par J-P. Billion chez Bull en France), et expliquons pourquoi ils permettent de faire les calculs nécessaires au passage à la grande échelle; nous mentionnons leurs limitations, qui sont inévitables car le calcul booléen est NP-complet. Les BDDs seront étudiés beaucoup plus en profondeur dans le cours 2015-2015. Pour terminer, nous montrons que le codage booléen permet de réaliser des optimisations très efficaces des circuits engendrés par les programmes Esterel. Nous insistons sur le fait que la structure du langage source et la façon d’y programmer les applications sont essentiels pour la qualité de l’optimisation finale : c’est grâce à l’interaction de la séquence, du parallélisme et de la préemption hiérarchique des comportements que les circuits engendrés par Esterel sont systématiquement meilleurs que ceux programmés et optimisés par les méthodes classiques, au moins en ce qui concerne leurs parties contrôle.

06 - Prouver les programmes : pourquoi, quand, comment ?  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Sixième leçon : Vérification et optimisation booléennes d'automates et circuits Ce dernier cours de 2014-2015 introduit les méthodes implicites de manipulation de systèmes de transitions, à travers les méthodes de calcul booléen utilisées à la fois pour la vérification formelles et pour l’optimisation de circuits électroniques et de programmes qui peuvent se réduire au calcul booléen. Ces méthodes ont révolutionné le domaine en permettant des vérifications formelles de systèmes dont le calcul explicite des états et transitions est impossible, car la taille des formules manipulées par les méthodes implicites est largement indépendante de celle des systèmes qu’ils décrivent. Nous expliquons d’abord les codages booléens d’ensembles, de relations et de fonctions, et montrons comment calculer l’image directe et l’image inverse de sous-ensembles par des fonctions. Nous étudions ensuite les codages booléens d’automates déterministes et non-déterministes, ainsi que leurs implémentations en circuits électroniques. Nous rappelons le fait que le circuit canoniquement associé à un automate non-déterministe est lui déterministe comme tous les circuits combinatoirement acycliques, ce qui montre clairement que le qualificatif « non-déterminisme » est particulièrement mal choisi : en vérification booléenne comme en optimisation de circuits, il est inutile de déterminiser les automates, et c’est souvent nuisible à cause de l’explosion exponentielle que la déterminisation peut produire. Nous montrons comment la vérification formelle de propriétés de sûreté définies par des observateurs se réduit au calcul des états accessibles, et comment effectuer ce calcul de manière implicite. Nous introduisons la première structure fondamentale du calcul booléen, les Binary Decision Diagrams, développés par R. Bryant au milieu des années 1980 (et indépendamment par J-P. Billion chez Bull en France), et expliquons pourquoi ils permettent de faire les calculs nécessaires au passage à la grande échelle; nous mentionnons leurs limitations, qui sont inévitables car le calcul booléen est NP-complet. Les BDDs seront étudiés beaucoup plus en profondeur dans le cours 2015-2015. Pour terminer, nous montrons que le codage booléen permet de réaliser des optimisations très efficaces des circuits engendrés par les programmes Esterel. Nous insistons sur le fait que la structure du langage source et la façon d’y programmer les applications sont essentiels pour la qualité de l’optimisation finale : c’est grâce à l’interaction de la séquence, du parallélisme et de la préemption hiérarchique des comportements que les circuits engendrés par Esterel sont systématiquement meilleurs que ceux programmés et optimisés par les méthodes classiques, au moins en ce qui concerne leurs parties contrôle.

05 - Prouver les programmes : pourquoi, quand, comment ? - PDF  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Sixième leçon : La vérification de modèles (model-checking) Ce cours termine la présentation générale des méthodes de vérification formelle par la vérification de modèles, plus connue sous son nom anglais original de model-checking. Cette méthode est bien différente des précédentes car elle s’intéresse essentiellement aux programmes d’états finis, ceux dont on peut au moins conceptuellement dérouler complètement toutes les exécutions possibles en temps et espace fini. De plus, contrairement aux méthodes précédemment décrites, le model-checking s’intéresse principalement aux programmes parallèles. Le parallélisme peut y être synchrone comme dans les circuits ou les langages synchrones présentés les années précédentes, ou asynchrones comme dans les protocoles de communication, les réseaux et les algorithmes distribués. Le model-checking est né au début des années 1980, quasi-simultanément en deux endroits : Grenoble avec J-P. Queille et J. Sifakis, qui ont développé le système CESAR et sa logique temporelle, et les USA avec E. Clarke et E. Emerson qui ont développé la logique temporelle CTL et le système EMV. Ces travaux ont donné le prix Turing 2007 à Clarke, Emerson et Sifakis. Ils s’appuyaient eux-mêmes sur les travaux d’Amir Pnueli (prix Turing en 1996) sur la logique temporelle. Le model-checking s’est considérablement développé ensuite, et constitue certainement la méthode formelle la plus utilisée dans l’industrie, en particulier dans la CAO de circuits. L’idée de base est de construire le graphe de toutes les exécutions possibles d’un programme, qu’on appelle son modèle. Ce modèle peut prendre la forme d’une structure de Kripke (logicien et philosophe de la logique modale), c’est-à-dire d’un graphe où les états sont étiquetés par des prédicats élémentaires, ou encore d’une structure de transitions, où les étiquettes sont portées par les transitions entre états. Une fois construit, le modèle devient indépendant du langage qui l’a engendré. Pour raisonner sur un modèle, un moyen très répandu est l’utilisation de logiques temporelles, définissent les propriétés temporelles à l’aide de propriétés élémentaires des états ou transitions et de quantificateurs sur les états ou les chemins de son graphe. On peut ainsi exprimer et vérifier des propriétés de sûreté (absence de bugs), comme « à aucun moment l’ascenseur ne peut voyager la porte ouverte », d’absence de blocages de l’exécution, ou de vivacité, comme « l’ascenseur finira par répondre à toutes les demandes des passagers » ou encore « chaque processus obtiendra infiniment souvent la ressource partagée s’il la demande infiniment souvent ». Nous présenterons d’abord la logique CTL*, la plus générale, qui permet d’imbriquer arbitrairement les quantifications d’états et de chemin sur les structures de Kripke. Mais cette logique très expressive est difficile à utiliser et les calculs y sont d’un coût prohibitif. Deux sous-logiques différentes sont utilisées : LTL (Linear Temporal Logic), qui ne quantifie pas sur les états et considère donc seulement des traces linéaires, et CTL, logique arborescente qui permet de quantifier sur les chemins mais avec des restrictions par rapport à CTL*. Ces deux logiques sont d’expressivités différentes et ont chacune des avantages et des inconvénients que nous discuterons brièvement. LTL est la logique la mieux adaptées pour la vérification de propriétés de vivacité, comme le montre L. Lamport (prix Turing 2014) avec son système TLA+. Mais, au contraire, elle ne permet pas d’exprimer des prédicats sur l’existence de calculs particuliers. La modélisation par systèmes de transitions, systématisée par R. Milner (prix Turing 1992) dans l’étude des calculs de processus communicants, permet de bien mieux composer les exécuti

05 - Prouver les programmes : pourquoi, quand, comment ?  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Cinquième leçon : La vérification de modèles (model-checking) Ce cours termine la présentation générale des méthodes de vérification formelle par la vérification de modèles, plus connue sous son nom anglais original de model-checking. Cette méthode est bien différente des précédentes car elle s’intéresse essentiellement aux programmes d’états finis, ceux dont on peut au moins conceptuellement dérouler complètement toutes les exécutions possibles en temps et espace fini. De plus, contrairement aux méthodes précédemment décrites, le model-checking s’intéresse principalement aux programmes parallèles. Le parallélisme peut y être synchrone comme dans les circuits ou les langages synchrones présentés les années précédentes, ou asynchrones comme dans les protocoles de communication, les réseaux et les algorithmes distribués. Le model-checking est né au début des années 1980, quasi-simultanément en deux endroits : Grenoble avec J-P. Queille et J. Sifakis, qui ont développé le système CESAR et sa logique temporelle, et les USA avec E. Clarke et E. Emerson qui ont développé la logique temporelle CTL et le système EMV. Ces travaux ont donné le prix Turing 2007 à Clarke, Emerson et Sifakis. Ils s’appuyaient eux-mêmes sur les travaux d’Amir Pnueli (prix Turing en 1996) sur la logique temporelle. Le model-checking s’est considérablement développé ensuite, et constitue certainement la méthode formelle la plus utilisée dans l’industrie, en particulier dans la CAO de circuits. L’idée de base est de construire le graphe de toutes les exécutions possibles d’un programme, qu’on appelle son modèle. Ce modèle peut prendre la forme d’une structure de Kripke (logicien et philosophe de la logique modale), c’est-à-dire d’un graphe où les états sont étiquetés par des prédicats élémentaires, ou encore d’une structure de transitions, où les étiquettes sont portées par les transitions entre états. Une fois construit, le modèle devient indépendant du langage qui l’a engendré. Pour raisonner sur un modèle, un moyen très répandu est l’utilisation de logiques temporelles, définissent les propriétés temporelles à l’aide de propriétés élémentaires des états ou transitions et de quantificateurs sur les états ou les chemins de son graphe. On peut ainsi exprimer et vérifier des propriétés de sûreté (absence de bugs), comme « à aucun moment l’ascenseur ne peut voyager la porte ouverte », d’absence de blocages de l’exécution, ou de vivacité, comme « l’ascenseur finira par répondre à toutes les demandes des passagers » ou encore « chaque processus obtiendra infiniment souvent la ressource partagée s’il la demande infiniment souvent ». Nous présenterons d’abord la logique CTL*, la plus générale, qui permet d’imbriquer arbitrairement les quantifications d’états et de chemin sur les structures de Kripke. Mais cette logique très expressive est difficile à utiliser et les calculs y sont d’un coût prohibitif. Deux sous-logiques différentes sont utilisées : LTL (Linear Temporal Logic), qui ne quantifie pas sur les états et considère donc seulement des traces linéaires, et CTL, logique arborescente qui permet de quantifier sur les chemins mais avec des restrictions par rapport à CTL*. Ces deux logiques sont d’expressivités différentes et ont chacune des avantages et des inconvénients que nous discuterons brièvement. LTL est la logique la mieux adaptées pour la vérification de propriétés de vivacité, comme le montre L. Lamport (prix Turing 2014) avec son système TLA+. Mais, au contraire, elle ne permet pas d’exprimer des prédicats sur l’existence de calculs particuliers. La modélisation par systèmes de transitions, systématisée par R. Milner (prix Turing 1992) dans l’étude des calculs de processus communicants, permet de bien mieux composer les exécu

04 - Prouver les programmes : pourquoi, quand, comment ? - PDF  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Quatrième leçon : Des logiques d'ordre supérieur à la programmation vérifiée en Coq Ce cours complète le précédent en terminant la présentation des méthodes générales de preuve de programmes par celle fondée sur les logiques d’ordre supérieur (celles où l’on peut aussi quantifier sur les prédicats) et sur le lambda-calcul déjà présenté en détail dans le cours 2009-2010. Nous montrons d’abord pourquoi l’ordre supérieur est plus expressif que l’ordre un. Par exemple, pour prouver une propriété par récurrence, il faut avoir en calcul des prédicats un schéma d’axiome de récurrence qui engendre un axiome particulier par prédicat à étudier, et donc une infinité d’axiomes ; en ordre supérieur, un seul axiome standard suffit puisqu’on peut quantifier universellement le prédicat de travail. D’autres avantages apparaîtront dans la suite du cours. Un inconvénient est bien sûr une plus grande complexité de la logique et de certains des algorithmes permettant de la traiter. Nous décrirons d’abord brièvement les systèmes HOL de M. Gordon, HOL-Light de J. Harrison, PVS de N. Shankar, S. Owre et J. Rushby, et Isabelle de L. Paulson, ce dernier étant en fait un méta-système logique dans lequel plusieurs logiques peuvent être définies. Ces systèmes ont conduit à des preuves très importantes en pratique : la preuve de correction de l’arithmétique entière et flottante du Pentium d’Intel par J. Harrison après le fameux bug de division du Pentium Pro qui a coûté 470 millions de dollars à Intel en 1994 ; la preuve de correction du micronoyau de système d’exploitation seL4 effectuée par G. Klein et. al. à NICTA Sydney en utilisant Isabelle (cf. le séminaire de D. Bolignano le 11 mars 2015 pour une autre preuve de système d’exploitation). Nous présentons ensuite avec plus de détails le système Coq, développé en France et titulaire de grandes récompenses récentes. Coq est fondé sur le calcul des constructions CoC de G. Huet et T. Coquand (1984) et sa version inductive CiC développée par C. Paulin, qui parlera en séminaire, à la suite de ce cours. Coq diffère des systèmes classiques par le fait qu’il intègre complètement calcul et preuve dans un formalisme très riche, incorporant et développant considérablement des idées et théorèmes de de Bruijn (Automath, 1967), Girard (SystemF, 1972), etc. Gallina, le langage de programmation de Coq est un langage typé d’ordre supérieur, c’est-à-dire dont les types peuvent eux-mêmes être des fonctions. Le typage est décidable, et le système de types garantit que tous les calculs de termes bien typés se terminent sur des formes normales uniques. La programmation classique est facilitée par la couche inductive, qui permet des définitions récursives puissantes mais à terminaison garantie. Grâce à la mise en pratique de la correspondance fondamentale de Curry-Howard entre calculs et preuves, il n’y a plus vraiment de différence entre calculer et prouver. Ainsi, un programme a pour type sa spécification alors qu’une preuve a pour type le théorème qu’elle démontre, ce de façon absolument identique. De plus, les preuves sont des fonctions standards du calcul, au même titre que les fonctions sur les types de données classiques. Enfin, une fois un programme développé et prouvé en Coq, on peut en extraire automatiquement un code objet directement exécutable écrit en Caml, correct par construction et normalement efficace. Tout cela donne à Coq une richesse considérable à la fois pour spécifier, programmer, prouver et exporter, quatre activités qui deviennent complètement intégrées. Le cours se terminera par la présentation de deux succès majeurs de Coq : d’abord le compilateur certifié CompCert de X. Leroy, seul compilateur C ayant passé le filtre des tests aléatoires présenté dans le cours du 4 mars ; ensuite la preuve complètement formelle de grands théorèmes mathématiques par G. Gonthier et. al., avec en particulier le fameux théorème de Feit-Thompson dont la preuve classique fait pas moins de 250 pages de lourdes mathématiques.

04 - Prouver les programmes : pourquoi, quand, comment ?  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Quatrième leçon : Des logiques d'ordre supérieur à la programmation vérifiée en Coq Ce cours complète le précédent en terminant la présentation des méthodes générales de preuve de programmes par celle fondée sur les logiques d’ordre supérieur (celles où l’on peut aussi quantifier sur les prédicats) et sur le lambda-calcul déjà présenté en détail dans le cours 2009-2010. Nous montrons d’abord pourquoi l’ordre supérieur est plus expressif que l’ordre un. Par exemple, pour prouver une propriété par récurrence, il faut avoir en calcul des prédicats un schéma d’axiome de récurrence qui engendre un axiome particulier par prédicat à étudier, et donc une infinité d’axiomes ; en ordre supérieur, un seul axiome standard suffit puisqu’on peut quantifier universellement le prédicat de travail. D’autres avantages apparaîtront dans la suite du cours. Un inconvénient est bien sûr une plus grande complexité de la logique et de certains des algorithmes permettant de la traiter. Nous décrirons d’abord brièvement les systèmes HOL de M. Gordon, HOL-Light de J. Harrison, PVS de N. Shankar, S. Owre et J. Rushby, et Isabelle de L. Paulson, ce dernier étant en fait un méta-système logique dans lequel plusieurs logiques peuvent être définies. Ces systèmes ont conduit à des preuves très importantes en pratique : la preuve de correction de l’arithmétique entière et flottante du Pentium d’Intel par J. Harrison après le fameux bug de division du Pentium Pro qui a coûté 470 millions de dollars à Intel en 1994 ; la preuve de correction du micronoyau de système d’exploitation seL4 effectuée par G. Klein et. al. à NICTA Sydney en utilisant Isabelle (cf. le séminaire de D. Bolignano le 11 mars 2015 pour une autre preuve de système d’exploitation). Nous présentons ensuite avec plus de détails le système Coq, développé en France et titulaire de grandes récompenses récentes. Coq est fondé sur le calcul des constructions CoC de G. Huet et T. Coquand (1984) et sa version inductive CiC développée par C. Paulin, qui parlera en séminaire, à la suite de ce cours. Coq diffère des systèmes classiques par le fait qu’il intègre complètement calcul et preuve dans un formalisme très riche, incorporant et développant considérablement des idées et théorèmes de de Bruijn (Automath, 1967), Girard (SystemF, 1972), etc. Gallina, le langage de programmation de Coq est un langage typé d’ordre supérieur, c’est-à-dire dont les types peuvent eux-mêmes être des fonctions. Le typage est décidable, et le système de types garantit que tous les calculs de termes bien typés se terminent sur des formes normales uniques. La programmation classique est facilitée par la couche inductive, qui permet des définitions récursives puissantes mais à terminaison garantie. Grâce à la mise en pratique de la correspondance fondamentale de Curry-Howard entre calculs et preuves, il n’y a plus vraiment de différence entre calculer et prouver. Ainsi, un programme a pour type sa spécification alors qu’une preuve a pour type le théorème qu’elle démontre, ce de façon absolument identique. De plus, les preuves sont des fonctions standards du calcul, au même titre que les fonctions sur les types de données classiques. Enfin, une fois un programme développé et prouvé en Coq, on peut en extraire automatiquement un code objet directement exécutable écrit en Caml, correct par construction et normalement efficace. Tout cela donne à Coq une richesse considérable à la fois pour spécifier, programmer, prouver et exporter, quatre activités qui deviennent complètement intégrées. Le cours se terminera par la présentation de deux succès majeurs de Coq : d’abord le compilateur certifié CompCert de X. Leroy, seul compilateur C ayant passé le filtre des tests aléatoires présenté dans le cours du 4 mars ; ensuite la preuve complètement formelle de grands théorèmes mathématiques par G. Gonthier et. al., avec en particulier le fameux théorème de Feit-Thompson dont la preuve classique fait pas moins de 250 pages de lourdes mathématiques.

03 - Prouver les programmes : pourquoi, quand, comment ? - PDF  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Troisième leçon : Les méthodes générales : assertions, réécriture, interprétation abstraite, logiques et assistants de preuve Il y a deux principaux types de méthodes formelles pour la preuve de programme : les méthodes générales, qui s’adressent à tous les types de programmes et seront présentées dans ce cours, et celles de la vérification de modèles (model-checking), qui s’intéressent principalement aux programmes à espaces d’états finis et aux circuits électroniques et seront traitées dans le cours no 5 du 25 mars 2015. La nécessité de traiter les programmes comme des objets mathématiques à part entière a été reconnue par A. Turing dès 1949. Il a alors introduit la notion d’assertion associant un prédicat logique à un point de contrôle du programme, ainsi que l’importance de la notion d’ordre bien fondé pour montrer la terminaison des programmes. Son approche par assertions est la première que nous traiterons dans le cours. Elle a été étendue et perfectionnée par R. Floyd, C.A.R. Hoare, E.W. Dijkstra, et bien d’autres, pour aboutir à une théorie et une pratique complètes de la définition logique des langages de programmation et de la vérification de programmes, applicables initialement aux programmes séquentiels impératifs. La notion d’assertion a été ensuite étendue en celle de contrat (assume/guarantee) à respecter par les fonctions ou modules d’un programme, applicable aussi aux langages objets et aux langages parallèles. En 1963, dans un article fondateur militant pour le traitement mathématique de la programmation et introduisant une brochette remarquable de nouveaux concepts, J. McCarthy a introduit l’idée bien différente d’utiliser la réécriture de termes comme outil applicable à la fois pour l’optimisation de programmes et leur vérification formelle. Cette approche, la seconde que nous étudierons, a eu une longue descendance dans les systèmes de vérification (Boyer&More, ACL2, PVS, Key, ProVerif, etc.), et continue d'irriguer les autres approches. Elle a eu des succès remarquables en circuits, en avionique, en sécurité, etc. La troisième approche historique est celle de la sémantique dénotationnelle des langages introduite par Scott et Strachey vers 1970. Ici, un programme est interprété comme une fonction dans un espace topologique ordonné par un ordre d’information, et toutes les fonctions sont rendues totales par l’ajout explicite d’éléments indéfinis. Une théorie générale du point fixe dans les espaces ordonnés permet d’interpréter de façon uniforme les boucles, la récursion et la programmation fonctionnelle d’ordre supérieur. Au début des années 1970, cette théorie a été à l’origine du pionnier des assistants de preuve de programmes, LCF, créé par Milner et al. Mais le traitement explicite de l’indéfini s’est révélé trop compliqué, et les assistants de preuve ont ensuite suivi un autre chemin. La sémantique dénotationnelle a cependant eu un succès considérable dans une autre approche de la vérification, l’interprétation abstraite créé par P. et R. Cousot en 1977. L’idée est ici de travailler avec des assertions portant non plus sur les valeurs exactes calculées, mais sur une abstraction de celles-ci, comme la preuve par 9 le fait pour détecter des erreurs dans la multiplication. De nombreux domaines abstraits ont été développés, ainsi que des méthodes algorithmiques générales de combinaison de ces domaines et d’accélération des calculs de points fixes. L’interprétation abstraite est maintenant développée industriellement. Elle a permis de vérifier des propriétés critiques de très gros programmes, comme l’absence d’erreurs à l’exécution dans le code de pilotage de l’Airbus A380. Elle est également utilisée pour l’évaluation du temps de calcul maximal de logiciels embarqués et pour accélérer les calculs dans d’autres types de système de vérification. La quatrième approche traitée dans ce cours est la vérification par assistants de preuves logiques. L’idée est ici de traduire le problème de vérification informatique en un problème purement logique, et de fournir une aide à la vérification à travers un système de tactiques et d’interaction homme-machine permettant d’organiser les preuves logiques à grand échelle, augmenté d’automatisations partielles pour des sous-domaines spécifiques utilisant par exemple des techniques de réécriture. Les assistants actuels traitent plusieurs types de logique, allant du calcul des prédicats de premier ordre augmenté par la théorie des ensembles (Rodin pour Event B, etc.) ou par la logique temporelle (TLA+), jusqu’aux calculs d’ordre supérieur (HOL, Isabelle, Coq, etc.). Ce cours présentera sommairement les ateliers de premier ordre, les ordres supérieurs étant traités dans le cours suivant. Nous prendrons l’exemple des formalismes B et Event-B de J.-R. Abrial (orateur du dernier séminaire du 1er avril 2015). L’atelier B a été utilisé pour l

03 - Prouver les programmes : pourquoi, quand, comment ?  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Troisième leçon : Les méthodes générales : assertions, réécriture, interprétation abstraite, logiques et assistants de preuve Il y a deux principaux types de méthodes formelles pour la preuve de programme : les méthodes générales, qui s’adressent à tous les types de programmes et seront présentées dans ce cours, et celles de la vérification de modèles (model-checking), qui s’intéressent principalement aux programmes à espaces d’états finis et aux circuits électroniques et seront traitées dans le cours no 5 du 25 mars 2015. La nécessité de traiter les programmes comme des objets mathématiques à part entière a été reconnue par A. Turing dès 1949. Il a alors introduit la notion d’assertion associant un prédicat logique à un point de contrôle du programme, ainsi que l’importance de la notion d’ordre bien fondé pour montrer la terminaison des programmes. Son approche par assertions est la première que nous traiterons dans le cours. Elle a été étendue et perfectionnée par R. Floyd, C.A.R. Hoare, E.W. Dijkstra, et bien d’autres, pour aboutir à une théorie et une pratique complètes de la définition logique des langages de programmation et de la vérification de programmes, applicables initialement aux programmes séquentiels impératifs. La notion d’assertion a été ensuite étendue en celle de contrat (assume/guarantee) à respecter par les fonctions ou modules d’un programme, applicable aussi aux langages objets et aux langages parallèles. En 1963, dans un article fondateur militant pour le traitement mathématique de la programmation et introduisant une brochette remarquable de nouveaux concepts, J. McCarthy a introduit l’idée bien différente d’utiliser la réécriture de termes comme outil applicable à la fois pour l’optimisation de programmes et leur vérification formelle. Cette approche, la seconde que nous étudierons, a eu une longue descendance dans les systèmes de vérification (Boyer&More, ACL2, PVS, Key, ProVerif, etc.), et continue d'irriguer les autres approches. Elle a eu des succès remarquables en circuits, en avionique, en sécurité, etc. La troisième approche historique est celle de la sémantique dénotationnelle des langages introduite par Scott et Strachey vers 1970. Ici, un programme est interprété comme une fonction dans un espace topologique ordonné par un ordre d’information, et toutes les fonctions sont rendues totales par l’ajout explicite d’éléments indéfinis. Une théorie générale du point fixe dans les espaces ordonnés permet d’interpréter de façon uniforme les boucles, la récursion et la programmation fonctionnelle d’ordre supérieur. Au début des années 1970, cette théorie a été à l’origine du pionnier des assistants de preuve de programmes, LCF, créé par Milner et al. Mais le traitement explicite de l’indéfini s’est révélé trop compliqué, et les assistants de preuve ont ensuite suivi un autre chemin. La sémantique dénotationnelle a cependant eu un succès considérable dans une autre approche de la vérification, l’interprétation abstraite créé par P. et R. Cousot en 1977. L’idée est ici de travailler avec des assertions portant non plus sur les valeurs exactes calculées, mais sur une abstraction de celles-ci, comme la preuve par 9 le fait pour détecter des erreurs dans la multiplication. De nombreux domaines abstraits ont été développés, ainsi que des méthodes algorithmiques générales de combinaison de ces domaines et d’accélération des calculs de points fixes. L’interprétation abstraite est maintenant développée industriellement. Elle a permis de vérifier des propriétés critiques de très gros programmes, comme l’absence d’erreurs à l’exécution dans le code de pilotage de l’Airbus A380. Elle est également utilisée pour l’évaluation du temps de calcul maximal de logiciels embarqués et pour accélérer les calculs dans d’autres types de système de vérification. La quatrième approche traitée dans ce cours est la vérification par assistants de preuves logiques. L’idée est ici de traduire le problème de vérification informatique en un problème purement logique, et de fournir une aide à la vérification à travers un système de tactiques et d’interaction homme-machine permettant d’organiser les preuves logiques à grand échelle, augmenté d’automatisations partielles pour des sous-domaines spécifiques utilisant par exemple des techniques de réécriture. Les assistants actuels traitent plusieurs types de logique, allant du calcul des prédicats de premier ordre augmenté par la théorie des ensembles (Rodin pour Event B, etc.) ou par la logique temporelle (TLA+), jusqu’aux calculs d’ordre supérieur (HOL, Isabelle, Coq, etc.). Ce cours présentera sommairement les ateliers de premier ordre, les ordres supérieurs étant traités dans le cours suivant. Nous prendrons l’exemple des formalismes B et Event-B de J.-R. Abrial (orateur du dernier séminaire du 1er avril 2015). L’atelier B a été utilisé pour l

02 - Prouver les programmes : pourquoi, quand, comment ? - PDF  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Deuxième leçon : De la spécification à la réalisation, au test et à la preuve : les approches formelles Ce premier cours du cycle « Prouver les programmes : pourquoi, quand, comment » a pour but d’introduire les méthodes formelles de développement et vérification de programmes, en les reliant aux méthodes de programmation, test et validation classiques. Dès les débuts de l’informatique, la difficulté de faire des programmes justes est apparue comme un problème majeur. Deux approches bien différentes ont été développées : d’une part, le génie logiciel, qui s’est développé lentement mais est maintenant bien en place au moins dans les entreprises sérieuses, et, d’autre part, une approche formelle beaucoup plus scientifique, introduite par Turing dès 1949 et fondée sur l’idée de voir un programme comme une entité mathématique sur laquelle il faut raisonner mathématiquement. C’est cette dernière qui a conduit aux méthodes formelles que nous étudierons cette année et les suivantes. Ces deux approches se sont développées très indépendamment l’une de l’autre et ne commencent à converger que depuis peu de temps : développement et vérification formels apparaissent désormais comme des moyens efficaces voire privilégiés d’éviter les bugs, au moins dans les applications où leur coût humain et matériel peut être catastrophique. Les techniques de vérification formelle ont eu une maturation assez lente, d’une part parce que le sujet est intrinsèquement difficile, d’autre part parce que l’industrie ne s’y est vraiment intéressée que récemment. Mais les choses bougent rapidement, avec des succès de plus en plus fréquents. Et, ce qui ne gâche rien pour un tel enseignement, les chercheurs français jouent un rôle majeur dans ce domaine en plein essor. Génie logiciel et vérification formelle partagent deux prérequis essentiels : d’abord, la qualité des spécifications initiales, qui doivent être précises, non-contradictoires, et complètes mais sans excès de précision inutile ; ensuite, la qualité des langages de programmation, dont la sémantique doit être précise tout en restant intuitive. Beaucoup de projets industriels échouent encore à cause de leur non-respect de ces contraintes. Le génie logiciel classique écrit les spécifications en langage habituel et fournit des outils de traçabilité permettant de relier spécifications et réalisation. Pour la validation du résultat, il s’appuie sur des revues de code et surtout sur des tests, ce qui pose deux problèmes majeurs : il est difficile de mesurer ce que les tests testent réellement, et le test n’apporte aucune information sur ce qui n’est pas testé. Mais nous verrons que des systèmes de génération de tests aléatoires dirigés permettent d’obtenir des résultats étonnants. À l’opposé, les méthodes formelles écrivent les spécifications en langage mathématique, le seul langage rigoureux dont nous disposions réellement, et font aussi progresser ce langage. Les systèmes modernes de typage des programmes permettent de détecter des erreurs dès les premières passes de compilation. Les meilleurs d’entre eux sont directement issus des recherches en sémantique de la programmation, elles-mêmes directement liées à la vérification formelle. Pour aller plus loin, on cherche à remplacer ou compléter les tests dynamiques de validation par des preuves statiques là encore mathématiques, aidées par des systèmes de vérification formelle plus ou moins automatisés. Au contraire des tests, la vérification formelle dit tout sur les propriétés à valider : prouvées vraies, elles le sont en toutes circonstances ; détectées comme fausses, les outils permettent souvent de construire des tests les invalidant et de découvrir ainsi la source de l’erreur. Mais la preuve, techniquement plus difficile que le test, demande une formation particulière. Et elle ne constitue pas forcément une panacée car certaines propriétés comme l’arrêt d’un programme ne sont pas prouvable en général (bien que les choses s’améliorent en pratique). Après avoir détaillé les problématiques ci-dessus, nous présenterons brièvement les styles de méthodes formelles qui seront détaillées dans la suite du cours, ainsi que leurs applications pratiques : assertions, preuves par réécritures sémantiques formelles, interprétation abstraite, vérifications logiques par assistants de preuve, et vérification automatique de modèles. Un point important de la discussion sera le lien avec la programmation classique. Nous verrons que trois points de vue assez différents coexistent naturellement, ce qui est une des raisons de la multiplicité des techniques précitées : Programmer comme d’habitude et utiliser les outils de vérification formelle pour complémenter les tests et vérifier un certain nombre de propriétés critique du programme (absence d’erreurs bloquant l’exécution, vérification de prédicats sur les états ou les sorties, etc.).

02 - Prouver les programmes : pourquoi, quand, comment ?  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Deuxième leçon : De la spécification à la réalisation, au test et à la preuve : les approches formelles Ce premier cours du cycle « Prouver les programmes : pourquoi, quand, comment » a pour but d’introduire les méthodes formelles de développement et vérification de programmes, en les reliant aux méthodes de programmation, test et validation classiques. Dès les débuts de l’informatique, la difficulté de faire des programmes justes est apparue comme un problème majeur. Deux approches bien différentes ont été développées : d’une part, le génie logiciel, qui s’est développé lentement mais est maintenant bien en place au moins dans les entreprises sérieuses, et, d’autre part, une approche formelle beaucoup plus scientifique, introduite par Turing dès 1949 et fondée sur l’idée de voir un programme comme une entité mathématique sur laquelle il faut raisonner mathématiquement. C’est cette dernière qui a conduit aux méthodes formelles que nous étudierons cette année et les suivantes. Ces deux approches se sont développées très indépendamment l’une de l’autre et ne commencent à converger que depuis peu de temps : développement et vérification formels apparaissent désormais comme des moyens efficaces voire privilégiés d’éviter les bugs, au moins dans les applications où leur coût humain et matériel peut être catastrophique. Les techniques de vérification formelle ont eu une maturation assez lente, d’une part parce que le sujet est intrinsèquement difficile, d’autre part parce que l’industrie ne s’y est vraiment intéressée que récemment. Mais les choses bougent rapidement, avec des succès de plus en plus fréquents. Et, ce qui ne gâche rien pour un tel enseignement, les chercheurs français jouent un rôle majeur dans ce domaine en plein essor. Génie logiciel et vérification formelle partagent deux prérequis essentiels : d’abord, la qualité des spécifications initiales, qui doivent être précises, non-contradictoires, et complètes mais sans excès de précision inutile ; ensuite, la qualité des langages de programmation, dont la sémantique doit être précise tout en restant intuitive. Beaucoup de projets industriels échouent encore à cause de leur non-respect de ces contraintes. Le génie logiciel classique écrit les spécifications en langage habituel et fournit des outils de traçabilité permettant de relier spécifications et réalisation. Pour la validation du résultat, il s’appuie sur des revues de code et surtout sur des tests, ce qui pose deux problèmes majeurs : il est difficile de mesurer ce que les tests testent réellement, et le test n’apporte aucune information sur ce qui n’est pas testé. Mais nous verrons que des systèmes de génération de tests aléatoires dirigés permettent d’obtenir des résultats étonnants. À l’opposé, les méthodes formelles écrivent les spécifications en langage mathématique, le seul langage rigoureux dont nous disposions réellement, et font aussi progresser ce langage. Les systèmes modernes de typage des programmes permettent de détecter des erreurs dès les premières passes de compilation. Les meilleurs d’entre eux sont directement issus des recherches en sémantique de la programmation, elles-mêmes directement liées à la vérification formelle. Pour aller plus loin, on cherche à remplacer ou compléter les tests dynamiques de validation par des preuves statiques là encore mathématiques, aidées par des systèmes de vérification formelle plus ou moins automatisés. Au contraire des tests, la vérification formelle dit tout sur les propriétés à valider : prouvées vraies, elles le sont en toutes circonstances ; détectées comme fausses, les outils permettent souvent de construire des tests les invalidant et de découvrir ainsi la source de l’erreur. Mais la preuve, techniquement plus difficile que le test, demande une formation particulière. Et elle ne constitue pas forcément une panacée car certaines propriétés comme l’arrêt d’un programme ne sont pas prouvable en général (bien que les choses s’améliorent en pratique). Après avoir détaillé les problématiques ci-dessus, nous présenterons brièvement les styles de méthodes formelles qui seront détaillées dans la suite du cours, ainsi que leurs applications pratiques : assertions, preuves par réécritures sémantiques formelles, interprétation abstraite, vérifications logiques par assistants de preuve, et vérification automatique de modèles. Un point important de la discussion sera le lien avec la programmation classique. Nous verrons que trois points de vue assez différents coexistent naturellement, ce qui est une des raisons de la multiplicité des techniques précitées : Programmer comme d’habitude et utiliser les outils de vérification formelle pour complémenter les tests et vérifier un certain nombre de propriétés critique du programme (absence d’erreurs bloquant l’exécution, vérification de prédicats sur les états ou les sorties, etc.).

01 - Prouver les programmes : pourquoi, quand, comment ? - PDF  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Première leçon : La révolution informatique dans les sciences L’informatique sert depuis longtemps de moyen de calcul dans les autres sciences, que ce soit en sciences de la nature ou en mathématiques. Mais un changement profond de vison de son rôle dans les sciences naturelles est en cours : la pensée algorithmique et ses réalisations informatiques apportent désormais un regard nouveau sur la façon d’étudier les phénomènes, et cela en particulier dans les sciences de la vie qui n’ont été historiquement que peu touchées par les approches mathématiques. Les techniques de modélisation et de simulation, originellement dédiées à la simple imitation du réel, deviennent des outils conceptuels et pratiques fondamentaux pour comprendre les phénomènes concernés. Elle conduisent à une nouvelle vision algorithmique des lois de la nature, où l’information et son calcul servent à représenter de façon uniforme les objets classiques d’étude que sont la matière, les ondes et l’énergie. Cette vision est fondée sur de nouvelles mathématiques discrètes qui complètent les mathématiques continues habituelles et ouvrent de nouveaux champs d’action, en fournissant des schémas de raisonnement bien différents des schémas classiques. Nous illustrerons ce propos par des exemple pris aussi bien en physique, géophysique et astronomie qu’en biologie et médecine. Enfin, nous montrerons comment l’informatique moderne commence à transformer aussi les mathématiques, à travers la possibilité de conduire désormais des preuves vraiment formelles de très grande taille, réalisées en machine à l’aide de systèmes informatiques fondés sur des logiques formelles très puissantes qui seront étudiées dans la suite du cours.

01 - Prouver les programmes : pourquoi, quand, comment ?  

Gérard Berry Algorithmes, machines et langages Année 2014-2015 Prouver les programmes : pourquoi, quand, comment ? Première leçon : La révolution informatique dans les sciences L’informatique sert depuis longtemps de moyen de calcul dans les autres sciences, que ce soit en sciences de la nature ou en mathématiques. Mais un changement profond de vison de son rôle dans les sciences naturelles est en cours : la pensée algorithmique et ses réalisations informatiques apportent désormais un regard nouveau sur la façon d’étudier les phénomènes, et cela en particulier dans les sciences de la vie qui n’ont été historiquement que peu touchées par les approches mathématiques. Les techniques de modélisation et de simulation, originellement dédiées à la simple imitation du réel, deviennent des outils conceptuels et pratiques fondamentaux pour comprendre les phénomènes concernés. Elle conduisent à une nouvelle vision algorithmique des lois de la nature, où l’information et son calcul servent à représenter de façon uniforme les objets classiques d’étude que sont la matière, les ondes et l’énergie. Cette vision est fondée sur de nouvelles mathématiques discrètes qui complètent les mathématiques continues habituelles et ouvrent de nouveaux champs d’action, en fournissant des schémas de raisonnement bien différents des schémas classiques. Nous illustrerons ce propos par des exemple pris aussi bien en physique, géophysique et astronomie qu’en biologie et médecine. Enfin, nous montrerons comment l’informatique moderne commence à transformer aussi les mathématiques, à travers la possibilité de conduire désormais des preuves vraiment formelles de très grande taille, réalisées en machine à l’aide de systèmes informatiques fondés sur des logiques formelles très puissantes qui seront étudiées dans la suite du cours.

Inaugural lecture : Mineral Resources, the Basis of Our Industrial Civilization: Major Challenges for the 21st Century  

Collège de France Georges Calas Sustainable Development - Environment, Energy and Society 2014-2015 Inaugural lecture : Mineral Resources, the Basis of Our Industrial Civilization: Major Challenges for the 21st Century

01 - Les ressources minérales, un enjeu majeur dans le contexte du développement durable - VIDEO  

Collège de France Georges Calas Développement durable – Environnement, énergie et société Année 2014-2015 Les ressources minérales, un enjeu majeur dans le contexte du développement durable Premier cours : Une approche multi-échelle des minéraux industriels

06 - Le temps élargi : horloges multiples, temps discrets et temps continu  

Gérard Berry Algorithmes, machines et langages Le temps élargi : horloges multiples, temps discrets et temps continu Sixième leçon : La déformatique

05 - Le temps élargi : horloges multiples, temps discrets et temps continu - PDF  

Gérard Berry Algorithmes, machines et langages Le temps élargi : horloges multiples, temps discrets et temps continu Cinquième leçon : Jouer avec le temps

05 - Le temps élargi : horloges multiples, temps discrets et temps continu  

Gérard Berry Algorithmes, machines et langages Le temps élargi : horloges multiples, temps discrets et temps continu Cinquième leçon : Jouer avec le temps

04 - Le temps élargi : horloges multiples, temps discrets et temps continu - PDF  

Gérard Berry Algorithmes, machines et langages Le temps élargi : horloges multiples, temps discrets et temps continu Quatrième leçon : L'électricité est constructive : l'équivalence entre la propagation électrique et le calcul Booléen constructif pour les circuits synchrones cycliques

04 - Le temps élargi : horloges multiples, temps discrets et temps continu  

Gérard Berry Algorithmes, machines et langages Le temps élargi : horloges multiples, temps discrets et temps continu Quatrième leçon : L'électricité est constructive : l'équivalence entre la propagation électrique et le calcul Booléen constructif pour les circuits synchrones cycliques

03 - Le temps élargi : horloges multiples, temps discrets et temps continu - PDF  

Gérard Berry Algorithmes, machines et langages Le temps élargi : horloges multiples, temps discrets et temps continu Troisième leçon : Coopération entre modèles de temps et de communication

0:00/0:00
Video player is in betaClose