Thèse Vérification Formelle d'Opérations sur des Modèles Géométriques Structurés H/F - Doctorat.Gouv.Fr

Établissement : Université Paris-Saclay GS Sciences de l'ingénierie et des systèmes École doctorale : Interfaces : matériaux, systèmes, usages Laboratoire de recherche : Mathématiques et Informatique pour la Complexité et les Systèmes - EA 4037 Direction de la thèse : Pascale LE GALL ORCID 0000000289556835 Début de la thèse : 2026-10-01 Date limite de candidature : 2026-05-22T23:59:59 Les systèmes de modélisation géométrique sont essentiels à l'informatique graphique, à la conception assistée par ordinateur et à la simulation. Ils permettent la représentation et la manipulation de formes complexes grâce à des représentations de données structurées (maillages, structures de demi-arêtes ou cartes combinatoires), qui rendent explicites les relations topologiques entre les sous-composantes des objets. l'application de séquences d'opérations de modélisation. Ces opérations peuvent être appliquées manuellement, automatiquement dans des pipelines de modélisation procédurale, ou, plus récemment, sélectionnées par des approches fondées sur les données, comme l'apprentissage par renforcement. Avec l'automatisation croissante de ces pipelines, un écart apparaît entre l'intention de haut niveau de l'utilisateur et l'implémentation de bas niveau des opérations, rendant les systèmes plus difficiles à comprendre, à déboguer et à valider.

Un défi majeur est de garantir que ces opérations préservent les propriétés structurelles, telles que la cohérence topologique. Deux approches complémentaires sont couramment utilisées. D'une part, les cadres de transformation de haut niveau permettent de spécifier les opérations sous forme de règles, souvent fondées sur la théorie des transformations de graphes, permettant un raisonnement formel sur leur exactitude au niveau sémantique. Cependant, ces garanties ne sont généralement pas liées aux implémentations. Par ailleurs, de nombreux systèmes reposent sur un petit ensemble d'opérations atomiques qui préservent les invariants par construction. Bien que robuste au niveau de l'implémentation, cette approche exige de s'assurer que les opérations de haut niveau sont correctement décomposées et que les primitives sont correctement implémentées, ce qui est rarement vérifié formellement et systématiquement. Ces approches révèlent un écart entre trois niveaux d'abstraction : les règles de transformation de haut niveau, les primitives de bas niveau et l'implémentations. Actuellement, il n'existe pas de cadre unifié pour relier ces niveaux et garantir la préservation des propriétés de correction entre eux. Ce problème est encore amplifié par l'utilisation de techniques automatisées, car les pipelines de transformation peuvent devenir opaques et difficiles à valider par de simples tests.

Cette thèse vise à étudier des méthodes formelles pour raisonner sur la correction des opérations de modélisation géométrique à différents niveaux d'abstraction. L'objectif est de comprendre comment les invariants structurels peuvent être spécifiés et préservés, des règles de haut niveau jusqu'aux implémentations, et comment les propriétés de correction locales peuvent être composées pour garantir la correction de systèmes de transformation complets. Le projet explorera en particulier des approches basées sur la vérification déductive et les assistants de preuve, adaptés au raisonnement sur les invariants structurels complexes et les systèmes de transformations non bornés. Les contributions attendues comprennent des modèles formels de systèmes de transformations géométriques, des principes de vérification soutenant le raisonnement compositionnel et une validation sur des scénarios de modélisation représentatifs. L'objectif est de jeter les bases de chaînes de traitement de modélisation géométrique plus fiables et explicables. Les systèmes de modélisation géométrique reposent sur des structures de données explicites, telles que les maillages ou les cartes combinatoires, ainsi que sur des opérations de transformation permettant de construire et modifier des objets complexes. Garantir la correction de ces opérations, en particulier la préservation d'invariants topologiques, constitue un enjeu majeur. Deux approches complémentaires coexistent : d'une part, des cadres de transformation de haut niveau fondés sur la théorie des transformations de graphes, permettant un raisonnement sémantique sur les opérations ; d'autre part, des approches basées sur des opérations primitives assurant la correction par construction. Cependant, ces niveaux d'abstraction restent aujourd'hui faiblement connectés, et les garanties obtenues à un niveau ne sont pas nécessairement préservées à l'implémentation. Ce projet s'inscrit à l'interface entre modélisation géométrique et méthodes formelles, et vise à développer des techniques de vérification permettant de raisonner de manière compositionnelle sur la correction des transformations à travers ces différents niveaux.
L'objectif de cette thèse de doctorat est d'étudier comment les propriétés de correction des opérations de modélisation géométrique peuvent être spécifiées et préservées à différents niveaux d'abstraction, depuis les règles de transformation de haut niveau jusqu'à leurs implémentations de bas niveau. Plus précisément, le projet étudiera comment exprimer les invariants structurels des représentations géométriques et comment composer et transférer les garanties de correction établies pour les opérations locales à des systèmes de transformation complets.

Le candidat doit être titulaire d'un master ou d'un diplôme d'ingénieur, avec une spécialisation en informatique. Il doit manifester un intérêt pour les méthodes formelles et le génie logiciel. Une connaissance préalable des outils utilisés pour la vérification formelle ou la modélisation géométrique serait un atout.