Étudiants recherchés pour plusieurs projets de maîtrise et de doctorat

Le Laboratoire d’informatique formelle de l’Université du Québec à Chicoutimi est à la recherche de candidats pour plusieurs projets financés de niveau maîtrise et doctorat débutant à l’été et à l’automne 2024. La Chaire de recherche du Canada en spécification, test et vérification de systèmes informatiques assure le financement des étudiants, sous la forme d’une bourse d’études, pour la durée du projet (2 ans pour la maîtrise, 3 ans pour le doctorat).

Projets proposés

Cliquer sur les liens ci-dessous pour une description plus détaillée de chacun des projets.

• LIF24-M1: Monitoring de l’économie des jeux vidéo. Vise à utiliser le simulateur machinations.io pour modéliser l’économie de jeux vidéo, simuler des scénarios pour équilibrer leur difficulté, et exporter les données pour analyse et transformation avec la librairie BeepBeep.
• LIF24-D1: Test et vérification pour l’event stream processing. Vise à développer la théorie, les techniques et les outils pour le test et la vérification formelle de programmes de flux, en particulier pour des pipelines de traitement dans des API comme BeepBeep.
• LIF24-D2: Évaluation des compétences cliniques par le monitoring et l’analyse de logs. Vise à formaliser, implémenter, et évaluer les mécanismes de mesure des compétences cliniques des infirmières par l’analyse de leurs actions dans un jeu, en utilisant des techniques d’analyse de logs et de méthodes formelles pour produire des indicateurs explicables pour l’amélioration continue.
• LIF24-D3: Détection d’anomalies dans un système de requêtes d’identité. Vise à analyser en temps réel les logs de requêtes d’identité dans un système sécurisé basé sur la blockchain pour détecter anomalies et comportements suspicieux, en utilisant la logique temporelle linéaire et la logique modale épistémique pour la modélisation formelle et la vérification pratique via un moniteur ou contrat intelligent.
• LIF24-D4: Suivi de la gestion de projet d’un jeu vidéo par l’analyse des fichiers de journalisation. Vise à développer des méthodes automatiques pour traiter les fichiers de journalisation dans le développement de jeux vidéo, afin de générer des alertes pour prévenir les problèmes et évaluer la santé du projet, ainsi qu’à identifier et ajuster automatiquement les éléments de journalisation nécessaires.

Les personnes souhaitant postuler sont invitées à remplir le formulaire en ligne à l’adresse https://zfrmz.com/BGLMrz4QFYzkIOZxVtpD en fournissant les éléments demandés.

Présentation établissement et labo d’accueil

L’Université du Québec à Chicoutimi (UQAC) fait partie du plus grand réseau universitaire au Canada. Elle est située dans la région francophone du Saguenay–Lac-Saint-Jean, réputée pour la beauté de son fjord et la majesté de sa nature environnante. L’UQAC accueille chaque année 6 500 étudiants, dont plus de 1 000 provenant de 50 pays différents. Le programme de recherche en informatique est particulièrement dynamique; il est l’hôte de deux chaires de recherche du Canada, comprend actuellement une vingtaine de professeurs, 30 doctorants et boursiers postdoctoraux et plus de 100 étudiants à la maîtrise.

Le travail de doctorat se déroulera au Laboratoire d’informatique formelle, sous la supervision du Pr. Sylvain Hallé, titulaire de la Chaire de recherche du Canada sur les tests, la spécifications et la vérification de systèmes informatiques. Le LIF est spécialisé dans l’application de méthodes formelles au test et à la vérification de divers systèmes logiciels. Les projets antérieurs des membres du corps professoral du LIF ont été réalisés en collaboration avec de nombreuses entreprises, dont Ericsson, Industrielle Alliance, Ubisoft LaForge, Devicom et Eckinox Média.

La recherche au LIF est reconnue internationalement et contribue au développement d’outils logiciels concrets et de haute qualité fondés sur des bases mathématiques solides. Les projets notables de longue date développés au LIF incluent le moteur de traitement de flux d’événements BeepBeep 3 [2], le système de surveillance de la blockchain Artichoke [3] et la bibliothèque de lignage de données Petit Poucet [4]. Toutes ces initiatives ont été récompensées et publiées dans des conférences internationales de premier plan au cours de la dernière décennie.

Références

1. A. Bédard, S. Hallé. (2021). Model Checking of Stream Processing Pipelines. In Proc. TIME, 5:1-5:17. DOI 10.4230/LIPIcs.TIME.2021.5
2. S. Hallé. (2018). Event Stream Processing with BeepBeep 3: Log Crunching and Analysis Made Easy. Presses de l’Université du Québec, ISBN 978-2-7605-5101-5
3. S. Hallé, R. Khoury, A. El-Hokayem, Y. Falcone. (2016). Decentralized Enforcement of Artifact Lifecycles. In Proc. EDOC, 1-10. DOI 10.1109/EDOC.2016.7579380
4. S. Hallé, H. Tremblay. (2021). Foundations of Fine-Grained Explainability. In Proc. CAV, Springer LNCS 12760, 500-523. DOI 10.1007/978-3-030-81688-9_24