Le problème abordé dans cette thèse concerne la productionautomatique de données de test permettant de prouver des propriétés de programmes. Nous nous situons ainsi à mi-chemin entre le domaine du test et celui de la vérification de programmes. Les travaux dans le domaine du test ont conduit à des outils semi-automatiques d'utilisation simple, mais qui reposent sur des hypothèses difficilement vérifiables en pratique. Dans le domaine de la vérification, des outils basés sur des méthodes formelles ont été développés, mais ils nécessitent un utilisateur expert dans les techniques de preuve utilisées par l'outil. Cette situation est due aux problèmes d'indécidabilité engendrés par la puissance des formalismes traités. La thèse que nous présentons est qu'il est possible de développer des méthodes formelles automatiques pour prouver des propriétés de programmes, à condition de considérer des formalismes restreints. Notre principale contribution est une nouvelle approche pour la vérification de programmes, intégrant les techniques de test et d'analyse statique. Nous proposons une méthode formelle de génération de jeux de test finis complets permettant de prouver qu'un programme vérifie une propriété donnée. Cette méthode utilise le texte du programme et de la propriété, qui doivent appartenir à certaines classes de programmes (ou de propriétés). Ces classes sont représentées par des hiérarchies de schémas, qui peuvent être vues comme modélisant des hypothèses de test. Tout programme appartenant à un de nos schémas et passant le jeu de test avec succès vérifie la propriété testée. Pour une propriété donnée, notre méthode est complètement automatique et ne nécessite donc aucune compétence particulière de l'utilisateur. Nous avons implanté cette méthode dans un prototype (traitant un langage fonctionnel restreint), pour le cas de propriétés s'exprimant en termes de longueurs de listes.

L'assimilation variationnelle de données 4D-Var est une technique très utilisée en géophysique, notamment en météorologie et océanographie. Elle consiste à estimer des paramètres d'un modèle numérique direct, en minimisant une fonction de coût mesurant l'écart entre les sorties du modèle et les mesures observées. La minimisation, qui est basée sur une méthode de gradient, nécessite le calcul du modèle adjoint (produit de la transposée de la matrice jacobienne avec le vecteur dérivé de la fonction de coût aux points d'observation). Lors de la mise en œuvre de l'AD 4D-Var, il faut faire face à des problèmes d'implémentation informatique complexes, notamment concernant le modèle adjoint, la parallélisation du code et la gestion efficace de la mémoire. Afin d'aider au développement d'applications d'AD 4D-Var, le logiciel YAO qui a été développé au LOCEAN, propose de modéliser le modèle direct sous la forme d'un graphe de flot de calcul appelé graphe modulaire. Les modules représentent des unités de calcul et les arcs décrivent les transferts des données entre ces modules. YAO est doté de directives de description qui permettent à un utilisateur de décrire son modèle direct, ce qui lui permet de générer ensuite le graphe modulaire associé à ce modèle. Deux algorithmes, le premier de type propagation sur le graphe et le second de type rétropropagation sur le graphe permettent, respectivement, de calculer les sorties du modèle direct ainsi que celles de son modèle adjoint. YAO génère alors le code du modèle direct et de son adjoint. En plus, il permet d'implémenter divers scénarios pour la mise en œuvre de sessions d'assimilation.Au cours de cette thèse, un travail de recherche en informatique a été entrepris dans le cadre du logiciel YAO. Nous avons d'abord formalisé d'une manière plus générale les spécifications deYAO. Par la suite, des algorithmes permettant l'automatisation de certaines tâches importantes ont été proposés tels que la génération automatique d'un parcours "optimal" de l'ordre des calculs et la parallélisation automatique en mémoire partagée du code généré en utilisant des directives OpenMP. L'objectif à moyen terme, des résultats de cette thèse, est d'établir les bases permettant de faire évoluer YAO vers une plateforme générale et opérationnelle pour l'assimilation de données 4D-Var, capable de traiter des applications réelles et de grandes tailles.

Les outils présentés dans ce mémoire ont pour but d'améliorer, par l'apport de méthodes et de techniques de calcul formel, les performances et les capacités de calcul des logiciels qui modélisent et le comportement dynamique de systèmes de corps mécaniques reliés entre eux. On s'intéresse à la possibilité d'écrire de manière automatique un ensemble d'équations différentielles régissant la dynamique de tels systèmes à partir de leurs descriptions physiques. Dans le premier chapitre, on décrit soigneusement les objets mécaniques et mathématiques qui interviennent dans l'étude dynamique des systèmes multicorps, et on met en évidence un problème fondamental : la nature de l'ensemble des configurations admissibles des mécanismes à structures bouclées. Le deuxième chapitre est une étude détaillée, sur un exemple, des différentes méthodes de génération des équations du mouvement de systèmes multicorps, dans l'optique de leur implémentation dans un logiciel de calcul symbolique. Il montre l'intérêt des techniques formelles et permet de spécifier les outils qui doivent être créés pour mener à bien cette implémentation. Dans le troisième chapitre, on présente les outils formels qui ont été développés pour aider à construire un générateur automatique des équations de la dynamique de systèmes polyarticulés. On se consacre, dans le quatrième chapitre, à apporter des éléments de solutions au problème de la détermination de la dimension des variétés de configurations de mécanismes à structures bouclées. Plusieurs méthodes faisant appel à des techniques algébriques, probabilistes et géométriques sont exposées, ainsi que leurs implémentations, et leurs expérimentations.

Dans cette thèse, nous abordons le problème de la génération automatique de contenu graphique avec un haut niveau de détails pour la génération de mondes. Dans cette quête du réalisme, les principaux verrous scientifiques et techniques sont : la gestion des masses de données géométriques nécessaires à la création de variétés d'objets naturels, la prise en compte des interactions en les différents objets et le contrôle utilisateur.Notre approche s'appuie sur un modèle volumique original et unificateur permettant de représenter les différents matériaux d'un terrain. Nous proposons un ensemble d'algorithmes de haut niveau, combinant des étapes de simulation pour assurer la plausibilité physique et le réalisme visuel à des techniques de génération procédurale permettant de gérer efficacement la complexité. Nos algorithmes permettent ainsi de sculpter des terrains complexes avec des grottes ou des surplombs et de générer des routes avec des tunnels et des ponts permettant le franchissement d'obstacles naturels. / In this thesis, we address the problem of automatic generation of graphical content with a high level of detail for the generation of worlds. In this quest for realism, the major scientific and technical challenges include: managing the mass of geometric data needed to create varieties of natural objects, taking into account interactions with the various objects and user control.Our approach is based on an original volumetric model for representing and unifying the different materials of land. We offer a range of high-level algorithms, combining simulation steps to ensure physical plausibility and visual realism, and procedural generation techniques to effectively manage complexity. Our algorithms are used to sculpt and complex terrain with caves and overhangs and generate roads with tunnels and bridges to cross natural barriers.

Les travaux présentés dans ce mémoire portent sur la validation de programmes PHP à travers un nouveau langage de spécification, accompagné de ses outils. Ces travaux s’articulent selon trois axes : langage de spécification, génération automatique de données de test et génération automatique de tests unitaires.La première contribution est Praspel, un nouveau langage de spécification pour PHP, basé sur la programmation par contrat. Praspel spécifie les données avec des domaines réalistes, qui sont des nouvelles structures permettant de valider etgénérer des données. À partir d’un contrat écrit en Praspel, nous pouvons faire du Contract-based Testing, c’est à dire exploiter les contrats pour générer automatiquement des tests unitaires. La deuxième contribution concerne la génération de données de test. Pour les booléens, les entiers et les réels, une génération aléatoire uniforme est employée. Pour les tableaux, un solveur de contraintes a été implémenté et utilisé. Pour les chaînes de caractères, un langage de description de grammaires avec un compilateur de compilateurs LL(⋆) et plusieurs algorithmes de génération de données sont employés. Enfin, la génération d’objets est traitée.La troisième contribution définit des critères de couverture sur les contrats.Ces derniers fournissent des objectifs de test. Toutes ces contributions ont été implémentées et expérimentées dans des outils distribués à la communauté PHP. / The works presented in this memoir are about the validation of PHPprograms through a new specification language, along with its tools. These works follow three axes: specification language, automatic test data generation and automatic unit test generation. The first contribution is Praspel, a new specification language for PHP, based on the Design by Contract. Praspel specifies data with realistic domains, which are new structures allowing to validate and generate data. Based on a contract, we are able to perform Contract-based Testing, i.e.using contracts to automatically generate unit tests. The second contribution isabout test data generation. For booleans, integers and floating point numbers, auniform random generation is used. For arrays, a dedicated constraint solver has been implemented and used. For strings, a grammar description language along with an LL(⋆) compiler compiler and several algorithms for data generation are used. Finally, the object generation is supported. The third contribution defines contract coverage criteria. These latters provide test objectives. All these contributions are implemented and experimented into tools distributed to the PHP community.

Le bâtiment devient de plus en plus un système complexe où les flux énergétiques doivent être gérés en fonction des usages : on parle de bâtiments intelligents. Il s'ensuit une complexité croissante pour les concepteurs, qui doivent s'intéresser autant au bâtiment lui-même (plusieurs sources électriques et multiplication des charges) qu'à ses équipements, sa gestion énergétique mais aussi aux interactions avec l'environnement extérieur (flux d'informations exogènes sur le marché d'énergie, prix d'achat et de revente, subventions à l'auto-consommation, etc...). Il est désormais nécessaire de coupler la phase de conception avec celle de gestion énergétique du bâtiment. Les travaux de cette thèse visent à proposer une démarche méthodologique permettant de formuler automatiquement les problèmes d'optimisation exploitables autant en conception qu'en exploitation du système bâtiment. La démarche est basée sur les concepts issus de l'ingénierie dirigée par les modèles (IDM). / The building is becoming increasingly a complex system where energy flows must be managed according to consumption: we talk about intelligent buildings. This means increasing complexity for designers who need to focus as much on building itself (several power sources and multiplication of charges) in its equipment, and in its energy management but also to interactions with the external environment (exogenous flow of information on the energy market, the purchase price and resale, subsidies for self-consumption, etc. ...). It is now necessary to tie the design phase with that of building energy management. The work of this thesis aims at proposing a methodological approach to automatically formulate optimization problems at design stage and under operation of building. The approach is based on concepts from the model-driven engineering (MDE).

La reconnaissance de la langue des signes française (LSF) comme une langue à part entière en 2005 a créé un besoin important de développement d’outils informatiques pour rendre l’information accessible au public sourd. Dans cette perspective, cette thèse a pour cadre la modélisation linguistique pour un système de génération de la LSF. Nous présentons dans un premier temps les différentes approches linguistiques ayant pour but la description linguistique des langues des signes (LS). Nous présentons ensuite les travaux effectués en informatique pour les modéliser.Dans un deuxième temps, nous proposons une approche permettant de prendre en compte les caractéristiques linguistiques propres au LS tout en respectant les contraintes d’un processus de formalisation. En étudiant des liens entre des fonctions sémantiques et leurs formes observées dans les corpus LSF, nous avons identifié plusieurs règles de production. Nous présentons finalement le fonctionnement des règles comme étant un système susceptible de modéliser un énoncé entier en LSF. / The recognition of French Sign Language (LSF) as a natural language in 2005 has created an important need for the development of tools to make information accessible to the deaf public. With this prospect, this thesis aims at linguistic modeling for a system of generation of LSF. We first present the different linguistic approaches aimed at describing the sign language (SL). We then present the models proposed in computer science. In a second step, we propose an approach allowing to take into account the linguistic properties of the SL while respecting the constraints of a formalisation process.By studying the links between semantic functions and their observed forms in LSF Corpora, we have identified several production rules. We finally present the rule functioning as a system capable of modeling an entire utterance in LSF.

Nos travaux s'inscrivent dans le domaine des résumés linguistiques flous (RLF) qui permettent la génération de phrases en langage naturel, descriptives de données numériques, et offrent ainsi une vision synthétique et compréhensible de grandes masses d'information. Nous nous intéressons d'abord à l'interprétabilité des RLF, capitale pour fournir une vision simplement appréhendable de l'information à un utilisateur humain et complexe du fait de sa formulation linguistique. En plus des travaux existant à ce sujet sur les composants élémentaires des RLF, nous proposons une approche globale de l'interprétabilité des résumés vus comme un ensemble de phrases et nous intéressons plus spécifiquement à la question de leur cohérence. Afin de la garantir dans le cadre de la logique floue standard, nous introduisons une formalisation originale de l'opposition entre phrases de complexité croissante. Ce formalisme nous permet de démontrer que les propriétés de cohérence sont vérifiables par le choix d'un modèle de négation spécifique. D'autre part, nous proposons sur cette base un cube en 4 dimensions mettant en relation toutes les oppositions possibles entre les phrases d'un RLF et montrons que ce cube généralise plusieurs structures d'opposition logiques existantes. Nous considérons ensuite le cas de données sous forme de séries numériques et nous intéressons à des résumés linguistiques portant sur leur périodicité : les phrases que nous proposons indiquent à quel point une série est périodique et proposent une formulation linguistique appropriée de sa période. La méthode d’extraction proposée, nommée DPE pour Detection of Periodic Events, permet de segmenter les données de manière adaptative et sans paramètre utilisateur, en utilisant des outils issus de la morphologie mathématique. Ces segments sont ensuite utilisés pour calculer la période de la série temporelle ainsi que sa périodicité, calculée comme un degré de qualité sur le résultat renvoyé mesurant à quel point la série est périodique. Enfin, DPE génère des phrases comme « Environ toutes les 2 heures, l'afflux de client est important ». Des expériences sur des données artificielles et réelles confirment la pertinence de l'approche. D’un point de vue algorithmique, nous proposons une implémentation incrémentale et efficace de DPE, basée sur l’établissement de formules permettant le calcul de mises à jour des variables. Cette implémentation permet le passage à l'échelle de la méthode ainsi que l'analyse en temps réel de flux de données. Nous proposons également une extension de DPE basée sur le concept de périodicité locale permettant d'identifier les sous-séquences périodiques d'une série temporelle par l’utilisation d’un test statistique original. La méthode, validée sur des données artificielles et réelles, génère des phrases en langage naturel permettant d’extraire des informations du type « Toutes les deux semaines sur le premier semestre de l'année, les ventes sont élevées ». / Our research is in the field of fuzzy linguistic summaries (FLS) that allow to generate natural language sentences to describe very large amounts of numerical data, providing concise and intelligible views of these data. We first focus on the interpretability of FLS, crucial to provide end-users with an easily understandable text, but hard to achieve due to its linguistic form. Beyond existing works on that topic, based on the basic components of FLS, we propose a general approach for the interpretability of summaries, considering them globally as groups of sentences. We focus more specifically on their consistency. In order to guarantee it in the framework of standard fuzzy logic, we introduce a new model of oppositions between increasingly complex sentences. The model allows us to show that these consistency properties can be satisfied by selecting a specific negation approach. Moreover, based on this model, we design a 4-dimensional cube displaying all the possible oppositions between sentences in a FLS and show that it generalises several existing logical opposition structures. We then consider the case of data in the form of numerical series and focus on linguistic summaries about their periodicity: the sentences we propose indicate the extent to which the series are periodic and offer an appropriate linguistic expression of their periods. The proposed extraction method, called DPE, standing for Detection of Periodic Events, splits the data in an adaptive manner and without any prior information, using tools from mathematical morphology. The segments are then exploited to compute the period and the periodicity, measuring the quality of the estimation and the extent to which the series is periodic. Lastly, DPE returns descriptive sentences of the form ``Approximately every 2 hours, the customer arrival is important''. Experiments with artificial and real data show the relevance of the proposed DPE method. From an algorithmic point of view, we propose an incremental and efficient implementation of DPE, based on established update formulas. This implementation makes DPE scalable and allows it to process real-time streams of data. We also present an extension of DPE based on the local periodicity concept, allowing the identification of local periodic subsequences in a numerical series, using an original statistical test. The method validated on artificial and real data returns natural language sentences that extract information of the form ``Every two weeks during the first semester of the year, sales are high''.

Music generation is a popular task in the domain of music artificial intelligence, aiming at generating music automatically. Music generation includes both symbolic and acoustic music generation. The former focuses on the score level, while the latter emphasizes the audio signal level. This thesis focuses on one task of symbolic music generation: generating symbolic melodies from lyrics and attempting to solve several pre-existing issues in this field. Firstly, we address the problem of melody generation from lyrics for non-popular music, which has not been widely studied in the literature, in addition to the generation of popular music. We study the following two music types: popular music with English lyrics and traditional Chinese music with classical Chinese poetry. The former has been extensively researched, while the latter has seldom been explored. Secondly, to mitigate the challenge of insufficient modeling of the relationship between lyrics and melody in non-popular music, we utilize deep neural networks to learn from a larger paired dataset for generating melodies from classical Chinese poetry. This approach enhances the model's ability to understand the relationship between classical Chinese poetry and its associated melodies. Another motivation behind this endeavor stems from historical context: many classical Chinese poems could be sung in ancient times, but many associated melodies have been lost, leaving only the poetry itself. Given the assumption that the lost melodies share similar elements, such as styles and genres, with the preserved melodies, this thesis employs deep neural networks to model the remaining melodies and their corresponding poems, which may assist in restoring these lost melodies. Thirdly, prior research integrates human music rules to enhance performance, which has limitations in generalization and adaptability. To tackle this issue, we employ methods allowing the model to autonomously encode music theory information for melody generation. Specifically, part-of-speech embeddings and tone embeddings are incorporated into the model, improving the capture of relationships between prosodic boundaries in lyrics (applicable to both English and Chinese lyrics) and melody, as well as between the tone of Chinese characters and the pitch of the melody, without manually designed rules. Fourthly, to address the problem of generated melodies lacking stylistic features, we incorporate style constraints into the inference phase. This adjustment enables the model to grasp the global style features of music to some extent. After implementing these adaptations, both objective and subjective evaluations are conducted. Objective ablation studies confirm that each adaptation contributes to improving the model's fit to the data. Subjective evaluations corroborate that our model can generate high-quality melodies akin to real music. / La génération de musique est une tâche populaire dans le domaine de l’intelligence artificielle musicale, visant à générer automatiquement de la musique. La génération musicale comprend la génération de musique symbolique et acoustique. La première se concentre sur le niveau de la partition, tandis que la seconde met l’accent sur le niveau du signal audio. Ce mémoire se concentre sur une tâche de génération musicale symbolique : générer des mélodies symboliques à partir de paroles et tenter de résoudre plusieurs problèmes existants dans ce domaine. Premièrement, nous abordons le problème de génération de la mélodie à partir de la parole pour la musique non populaire, un problème assez peu étudié. Nous étudions non seulement la génération de la musique populaire à partir de la parole en anglais, mais aussi et surtout de la musique chinoise traditionnelle avec de la poésie classique. La première a fait l’objet de nombreuses recherches, tandis que la dernière a rarement été explorée. Deuxièmement, pour atténuer le défi de la modélisation insuffisante de la relation entre les paroles et la mélodie dans la musique non populaire, nous utilisons des réseaux neuronaux profonds pour apprendre à partir d’un ensemble de données appariées plus grand pour générer des mélodies à partir de la poésie chinoise classique. Cette approche renforce la capacité du modèle à comprendre la relation entre la poésie chinoise classique et ses mélodies associées. Une autre motivation derrière cette démarche provient du contexte historique : de nombreux poèmes chinois classiques pouvaient être chantés dans l’Antiquité, mais de nombreuses mélodies associées ont été perdues, ne laissant que la poésie elle-même. En supposant que les mélodies perdues partagent des éléments similaires, tels que les styles et les genres, avec les mélodies préservées, ce mémoire utilise des réseaux neuronaux profonds pour modéliser les mélodies restantes et leurs poèmes correspondants, ce qui peut aider à restaurer ces mélodies perdues. Troisièmement, la recherche précédente intègre des règles musicales humaines pour améliorer les performances, ce qui a des limitations en matière de généralisation et d’adaptabilité. Nous employons des méthodes permettant au modèle de coder de manière autonome des informations théoriques sur la musique pour la génération de mélodies. Plus précisément, des plongements de parties du discours et des plongements de tons sont intégrés au modèle, améliorant la capture des relations entre les frontières prosodiques dans les paroles (applicables à la fois aux paroles anglaises et chinoises) et la mélodie, ainsi qu’entre le ton des caractères chinois et la hauteur de la mélodie, sans règles conçues manuellement. Quatrièmement, pour aborder le problème du manque de caractéristiques stylistiques des mélodies générées, nous intégrons des contraintes de style dans la phase d’inférence. Cet ajustement permet au modèle de saisir dans une certaine mesure les caractéristiques stylistiques globales de la musique. Après avoir mis en œuvre ces adaptations, des évaluations objectives et subjectives sont menées. Les études objectives d’ablation confirment que chaque adaptation contribue à améliorer l’ajustement du modèle aux données. Les évaluations subjectives corroborent que notre modèle peut générer des mélodies de haute qualité semblables à de la vraie musique.

Ce mémoire de maîtrise présente le développement d’un système de génération de la langue naturelle pour automatiser les lettres de contact envoyées par les chasseurs de tête. Les travaux de Ehud Reiter ont inspiré la portion de génération de texte. La génération du contenu est basée sur des règles d’associations obtenues par l’analyse statistique d’une base de données de profils LinkedIn. Le système écrit des lettres en anglais mais peut être facilement étendu à la langue française. Ce projet s’inscrit dans le cadre du Butterfly Predictive Project, une collaboration entre l’Université de Montréal et LittleBIGJob. / This master’s thesis presents the development of a Natural Language Generation system designed to automate the writing of first-contact letters by professional headhunters. A top-down approach modelled on Ehud Reiter’s work handles the Natural Language portion of the system. Content generation is based on association rules obtained by statistical analysis of a large database of LinkedIn profiles. The system writes English letters but can easily be extended to French. This project is part of the Butterfly Predictive Project, a collaboration between Université de Montréal and LittleBIGJob.