Session executive education Apprentissage automatique, les briques technologiques pour les PME spéciale IA générative le 1er avril – GRATUIT !

Session deeptech Analyse des données de santé sensibles par l’apprentissage fédéré le 2 avril

Session état de l’art Cyberattaques dans les réseaux sans fils : quel impact, quels enjeux ? le 9 avril

Session état de l’art Les dispositifs médicaux intégrant de l’IA : challenges méthodologiques et règlementaires le 16 avril – NOUVEAU !

Session deeptech Scikit-learn, la boîte à outils de l’apprentissage automatique niveau 2 les 21 et 22 avril

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

Rocq, la preuve par le logiciel

Le système Rocq-prover, nommé auparavant l'assistant de preuve 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 Rocq-prover 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 Rocq-prover et qui servent de base à des projets de plus en plus ambitieux.

À l’issue de la formation, 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 Rocq ;
  • 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

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

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

Public cible : 

Pré-requis

Module débutant du cours.

Programme

Le programme de 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.

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

2
1700 / pers.

Aucune session disponible actuellement.

Contactez-nous

Pour aller plus loin

Informations pratiques

  • Durée : 1 jour (6h).
  • Horaires : 9h-12h / 13h30-16h30.
  • Délais d’accès : les inscriptions s’arrêtent 15 jours avant la date affichée.

  • Informations sur l’admission : l’admission au cours fait l’objet d’une sélection préalable.  

  • Format : toutes les sessions en dehors de l’intra-entreprise se déroulent en distanciel.

  • Modalités pédagogiques : la formation est délivrée en distanciel, en langue française avec les supports en anglais. Le cours peut se dérouler en anglais si tous les participants sont anglophones. La taille du groupe : 12 personnes maximum.

  • Privatisation du module (session intra-entreprise) : à partir de 5 personnes. Nous contacter via le formulaire de contact.

  • Moyens pédagogiques : le support du cours sera fourni aux participants.

  • Modalités d’évaluation et de suivi : l’évaluation est assurée par les quizz. Une attestation de formation est délivrée à la fin du parcours.

  • Accessibilité – handicap : Inria s’engage à garantir l’accessibilité de ses formations à distance et en présentiel aux personnes en situation de handicap. Plus de détails

 

À propos des tarifs

  • Module niveau 1 (1 jour) : 800 € par personne
  • Module niveau 2 (2 jours) : 1700 € par personne
  • Tarifs dégressifs à partir de 5 personnes (-10% de 5 à 9 inscrits, -20% plus de 10 inscrits)
  • Tarif dégressif pour les entreprises membres du pôle Aktantis (-20%)
  • Modalités de financement : fonds propres

Découvrir

Demander plus d'informations