Nouveau module ! Masterclass executive education Transition vers une cryptographie sûre dans un monde post-quantique le 24 avril

Prochaine session deeptech SOFA, le moteur de simulation multiphysique débutant le 25 avril

Nouveau module ! Formation état de l’art La sécurité informatique face aux menaces quantiques le 25 avril

Prochaine session deeptech Machine Learning and Cybersecurity: Why and How with scikit-learn avancé les 29 avril et 6 mai

Nouveau module ! Formation état de l’art La cybersécurité des systèmes de contrôle industriel le 29 avril

Toutes nos formations
démonstration sur ordinateur Méthodes formelles

Coq, la preuve par le logiciel

Le système Coq fournit un langage de programmation simplifié pour décrire des algorithmes, les propriétés logiques de ces algorithmes, et les preuves que les propriétés logiques sont satisfaites. La caractéristique clé de ce langage est une version approfondie du typage comme on le trouve dans les langages de programmation conventionnels. Bien que simplifié, ce langage est assez puissant pour décrire des logiciels avancés, comme une machine virtuelle Java, un compilateur C ou un microprocesseur. © Inria / Photo C. Morel

Session:

Aucune session disponible actuellement.

Contactez-nous !

Objectifs

Ce cours s’adresse à des ingénieurs en informatique ayant une expérience du développement logiciel dans un langage de programmation usuel. Le cours comporte sept volets pour enseigner :

  • la base de la théorie des types,
  • comment décrire des algorithmes,
  • comment exprimer les propriétés attendues,
  • comment prouver que les propriétés sont satisfaites,
  • comment tirer parti de la modularité logique,
  • comment obtenir du logiciel exécutable,
  • un panorama des applications complètes et réalistes.

Il s’inspire du cas de figure des bases de données pour montrer comment appliquer Coq pour modéliser des opérations sur des ensembles de données (intersection, union, sélection). Les propriétés logiques illustrent comment plusieurs séquences d’opérations peuvent aboutir au même résultat. Les techniques de preuves se concentrent sur les connecteurs logiques de base et sur la technique qui permet de raisonner sur des ensembles de taille non bornée: la preuve par récurrence. Le cours montre également comment des choix de structure de données différents permettent d’obtenir des programmes plus ou moins efficaces, tout en préservant la correction des opérations effectuées. Les techniques pour obtenir du code exécutable à partir des modèles formels sont également présentées. Enfin, le cours effectue un panorama des applications majeures qui ont été développées avec Coq et qui servent de base à des projets de plus en plus ambitieux.

À la fin du cours, les participants auront compris comment les techniques de modélisation, de description des propriétés, de preuve, et de production de logiciel dérivé peuvent être appliquées sur des projets logiciels.

Pré-requis

Savoir coder de petits algorithmes dans des langages de programmation usuels.

Programme

Ensembles finis et listes

  • programmation fonctionnelle avec des listes typées ;
  • la construction de filtrage, la récursion ;
  • opérations de base sur les ensembles finis.

Expressions logiques et spécifications

  • les connecteurs logiques ;
  • propriétés logiques des ensembles finis ;
  • quelques équivalences utiles entre constructions logiques.

Techniques de preuve

  • raisonnement sur les connecteurs logiques ;
  • raisonnement sur les constructions de programmation ;
  • techniques de preuve par récurrence.

Structures de données avancées

  • limites calculatoires des listes ;
  • structures de données arborescentes efficaces ;
  • nombres et arbres binaires ;
  • avantages de la modularité logique.

Exécution et extraction des programmes

  • modalités et limites de l’exécution dans Coq ;
  • extraction et exécution des programmes extraits ;
  • raisonner sur des programmes C.

Un tour d’horizon des applications marquantes

Intervenant(s)

  • Yves Bertot

    Directeur de recherche Inria

    Directeur de recherche Inria, Yves Bertot est spécialisé dans les preuves en théorie des types, étudiant successivement les propriétés des langages de programmation, la géométrie algorithmique, les calculs mathématiques et les interactions entre preuve formelle et calcul formel algébrique. Il a coécrit avec Pierre Castéran le premier livre sur le système Coq qui a été publié en 2004, Interactive Theorem Proving And Program Development, Coq’art: The Calculus Of Inductive Constructions. Il a participé à certains des résultats les plus remarquables obtenus avec le système Coq, comme le compilateur CompCert et la preuve vérifiée sur ordinateur du théorème de l’ordre impair.

    © Inria / Photo C. Lebedinsky

  • Pierre Boutry

    Chercheur postdoctoral Inria

    Chercheur postdoctoral chez Inria, Pierre Boutry s’intéresse aux fondements de la géométrie et à leur formalisation au sein du système Coq à l’aide de la librairie Mathematical Components. Il a obtenu un doctorat à l’université de Strasbourg en 2018 sur les façons d’axiomatiser la géométrie euclidienne, les énoncés du postulat des parallèles ainsi que les possibilités d’automatiser le raisonnement géométrique. Il a notamment contribué à la découverte d’une nouvelle preuve d’indépendance du postulat des parallèles.

    © Inria / coll. part.

Les prochaines sessions

1 jour

Session:

Aucune session disponible actuellement.

Contactez-nous !

Objectifs

Dans ce module avancé, les stagiaires ont l’opportunité de mettre en œuvre le langage de programmation de Coq pour modéliser des algorithmes simples, d’écrire des propriétés que ces algorithmes doivent satisfaire, et de produire des preuves formelles vérifiées par Coq.

Ce cours est organisé en six volets:

  • Définir des structures de données et des programmes pour produire et manipuler ces structures de données. En particulier, ce volet permettra aux étudiants de maîtriser les contraintes de la récursion structurelle et les avantages du polymorphisme.
  • Maîtriser les connecteurs logiques et leur application à programmation. En particulier, ce volet présente la distinction entre propriétés décidables et propriétés logiques indécidables, logique intuitionniste et logique classique.
  • Effectuer des preuves interactives. Ce cours donnera le temps aux étudiants d’acquérir les techniques de preuves dirigées par les buts, les techniques de preuves associées aux différents moyens de programmation et aux différents connecteurs logiques. Enfin, ce cours décrira les moyens pour exploiter les bibliothèques existantes de résultats mathématiques en Coq.
  • Connaître les domaines d’application des outils de preuve automatique. Ce cours fera un tour d’horizon de techniques de preuve automatique existante dans l’environnement de travail de Coq. Il inclura également une initiation aux techniques d’automatisation de conception de nouvelles procédures de décision.
  • Exploiter le pouvoir expressif des types dépendants. Dans ce cours, les étudiants seront initiés aux techniques permettant de mélanger données et preuves dans de nouveaux types de données plus informatifs.
  • Le sixième volet sera constitué d’une session d’apprentissage sur machine où les étudiants pourront se concentrer sur une série d’exercices de difficulté progressive.

À l’issue du cours, les utilisateurs seront en mesure de décrire des algorithmes élémentaires et de faire des preuves sur ces algorithmes.

Pré-requis

Module débutant du cours.

Intervenant(s)

  • Yves Bertot

    Directeur de recherche Inria

    Directeur de recherche Inria, Yves Bertot est spécialisé dans les preuves en théorie des types, étudiant successivement les propriétés des langages de programmation, la géométrie algorithmique, les calculs mathématiques et les interactions entre preuve formelle et calcul formel algébrique. Il a coécrit avec Pierre Castéran le premier livre sur le système Coq qui a été publié en 2004, Interactive Theorem Proving And Program Development, Coq’art: The Calculus Of Inductive Constructions. Il a participé à certains des résultats les plus remarquables obtenus avec le système Coq, comme le compilateur CompCert et la preuve vérifiée sur ordinateur du théorème de l’ordre impair.

    © Inria / Photo C. Lebedinsky

  • Pierre Boutry

    Chercheur postdoctoral Inria

    Chercheur postdoctoral chez Inria, Pierre Boutry s’intéresse aux fondements de la géométrie et à leur formalisation au sein du système Coq à l’aide de la librairie Mathematical Components. Il a obtenu un doctorat à l’université de Strasbourg en 2018 sur les façons d’axiomatiser la géométrie euclidienne, les énoncés du postulat des parallèles ainsi que les possibilités d’automatiser le raisonnement géométrique. Il a notamment contribué à la découverte d’une nouvelle preuve d’indépendance du postulat des parallèles.

    © Inria / coll. part.

2 jours
910 / pers.

Aucune session disponible actuellement.

Contactez-nous

Pour aller plus loin

À propos des tarifs

  • Partenariat avec le pôle Systematic et le pôle SCS : les entreprises membres du pôle bénéficient d’un tarif privilégié,
  • Module débutant (1 jour) : 930 € par personne (740 € pour les entreprises membres des pôles partenaires),
  • Module avancé (2 jours) : 1300 € par personne (1040 € pour les entreprises membres des pôles partenaires),
  • Tarifs dégressifs à partir de 5 personnes (-10% de 5 à 9 inscrits, -20% plus de 10 inscrits) et en cas d’achat groupé des modules débutant et avancé (-20%),
  • Toutes les sessions en dehors de l’intra-entreprise se déroulent en distanciel.

Découvrir

Demander plus d'informations