Modèles de calcul

Parcours IL / Orientation MFLS

Alors que les modèles de calculs classiques donnent une définition précise des fonctions calculables, ils sont inopérants lorsqu’on s’intéresse à un système pouvant interagir avec des objets infinis ou semi-infinis, comme des streams dans un langage de programmation ou des entrées continues. De plus, ils ne permettent de manipuler que de manière limitée la notion de ressource, qu’elle soit classique (temps, mémoire) ou quantique (intrication).

Ce cours offre une introduction aux techniques et outils permettant de raisonner et manipuler ce type d’objets. Une première partie expliquera comment représenter et manipuler des réels, des fonctions ou des qubits (bits quantiques), soit de façon intrinsèque en utilisant un modèle de calcul adapté (automates cellulaires, modèle BSS, circuits quantiques) ou extrinsèque en les représentant comme des suites binaires infinies (machines de Turing). Une deuxième partie expliquera comment mesurer de façon statique les ressources, comme le temps, l~espace mémoire ou l~intrication, utilisées par un calcul.

Prérequis

  • Notions de complexité et de calculabilité.

Acquis d’apprentissage

  • Calcul sur des objets infinis: représentation et manipulation des nombres réels, des fonctions et des flux de données par suites binaires infinies.
  • Nouveaux modèles de calcul : automates cellulaires, calcul quantique.
  • Ressources du calcul: évaluation statique des ressources d’un processus, complexité  d’ordre supérieur.

Compétences visées

  • Maîtriser et mettre en œuvre les méthodes formelles pour la spécification ou modélisation d’un problème donné, la preuve et la vérification de propriétés dans le contexte de la sûreté et la sécurité logicielle.
  • Concevoir et développer des approches formelles adaptées, leur combinaison et des outils associés, pour la certification de systèmes complexes.
  • Concevoir des programmes manipulant des objets continus, des fonctions, des qubits.
  • Évaluer a priori les ressources classiques et quantiques utilisées par un programme.

Parcours IL / Orientation MFLS