Réunion scientifique Les Angles 2019
Journées scientifiques de préparation pour le dépôt d'un projet de recherche sur la vérification formelle de systèmes.
Liste des participants
- ENS Paris: Marc Pouzet.
- ENSTA ParisTech: Julien Alexandre dit Sandretto, Jason Brown, Alexandre Chapoutot, Olivier Mullier.
- IRIT: Xavier Thirioux, Alexis ?, Érik Martin-Dorel
- ONERA Toulouse: Arnaud Dieumegard, Pierre-Loïc Garoche, Charles Poussot-Vassal, Paul Rousse, Pierre Roux.
- Numalis: Arnault Ioulalen.
- Université Paris-Saclay: Sylvain Conchon, Guillaume Melquiond.
- Université de Perpignan: Assalé Adjé, Dorra Benkhalifa, Farah Benmouhoub, Asma Mansouri, Matthieu Martel, Katia M'Zyene.
Programme des journées
-
Journée du 6 février 2019
- 16h00 - 16h30 : Farah Benmouhoub
- 16h30 - 17h30 : Érik Martin-Dorel et Pierre Roux
- 17h30 - 18h00 : Asma Mansouri
-
Journée du 7 février 2019
- 09h30 - 10h00 : Pierre-Loïc Garoche et Charles Poussot-Vassal
- 10h00 - 10h30 : Paul Rousse et Pierre-Loïc Garoche
- 10h30 - 11h30 : Arnault Ioulalen
- 11h30 - 12h00 : Matthieu Martel
-
Journée du 8 février 2019
- 09h30 - 10h00 : Olivier Mullier
- 10h00 - 11h00 : Assalé Adjé
- 11h00 - 12h00 : Marc Pouzet
Liste des exposés (orateur, titre, et résumé)
-
Érik Martin-Dorel et Pierre Roux: Flottants primitifs en Coq (1h)
Certaines preuves mathméatiques requièrent des calculs intensifs, par exemple : théorème des quatre couleurs, théorème de Hales (ex conjecture de Kepler sur l'empilement des sphères), arithmétique d'intervalles. Pour des calculs numériques, l'usage de l'arithmétique à virgule flottante s'est imposé par son efficacité, malgré l'introduction d'erreurs d'arrondis.
On peut obtenir des garanties formelles sur des algorithmes flottants en s'appuyant sur la norme IEEE754, qui spécifie précisément l'arithmétique flottante et ses modes d'arrondis, et sur un assistant de preuve tel que Coq, qui possède des capacités de calcul efficace. Coq supporte en particulier les entiers machines, toutefois l'arithmétique flottante est actuellement émulée grâce à ces entiers.
Nous présentons dans cet exposé une modification de Coq permettant d'utiliser les opérations flottantes du processeur. Nous verrons quels sont les principaux obstacles à surmonter dans une telle implémentation. Les premiers benchmarks montrent un gain potentiel d'au moins deux ordres de grandeur.
-
Olivier Mullier: Instants de commutation optimaux pour la commande de systèmes hybrides (30')
Cette présentation traitera le ploblème de détermination des instants de commutation de systèmes hybrides commandés sous contrainte d'atteignabilité et optimisation d'un certain coùt. Ce problème est traité sous la forme d'un problème d'optimisation globale intervalle faisant intervenir des contraintes differentielles. Sa résolution passe par des techniques de simulation ensembliste garantie et un maillage du temps. Cette approche sera illustrée par deux exemples dont la résolution du problème de Goddard (une roquette doit atteindre une certaine altitude tout en consommant le minimum de carburant).
-
Marc Pouzet: Programmation synchrone probabiliste (1h)
-
Arnault Ioulalen: CALVINN - Validation formelle de la robustesse de réseaux de neurones. État des lieux des résultats scientifiques et du programme de normalisation en cours. (1h)
-
Assalé Adjé: systèmes dynamiques perturbés et optimisation stochastique (1h)
-
Asma Mansouri: Fixed Point Computation by Exponentiating Linear Operators (30')
-
Farah Benmouhoub: Static Analysis and Program Transformation for Numerical Accuracy in MPI (30')
-
Matthieu Martel: Great Neuron Savings! (30')
-
Pierre-Loïc Garoche et Charles Poussot-Vassal: Towards a proper characterization of hybrid discrete/continuous time linear systems (30')
On s'intéresse à ces systèmes temps continu, temps discret. On cherche à définir proprement la sémantique de la boucle fermée. Dans le cas de dynamiques linéaires, tant du coté temps continu que temps discret, nous proposons d'exprimer cette dynamique comme la solution d'un système linéaire à retards satisfaisant des contraintes algébriques.
-
Paul Rousse et Pierre-Loïc Garoche: Simulation ensembliste alternée de systèmes temps continus-temps discrets (30')
L'objectif est de mettre au point des outils de simulation des états atteignables d'un système qui combine un système dynamique à temps continu avec un controleur en temps discret. Il existe pour les systemes dynamiques des outils permettant d'obtenir des inegalités sur les états atteignables. Coté discret, nous sommes également capable de calculer des invariants sur les états atteignables. Il est délicat de calculer des propriétés sur le système complet. Nous souhaitons donc alternativement propager des ensembles de chaque coté pour caractériser les états atteignables sur un intervalle de temps donné.