Home › Postes ouverts › Étudiants recherchés pour plusieurs projets de maîtrise et de doctorat

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

Posted on by by Posted in Postes ouverts

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
Tags: , , ,

Students wanted for several master’s and doctoral projects

Posted on by by Posted in Open positions, Postes ouverts, Uncategorized

The Formal Computing Laboratory of the Université du Québec à Chicoutimi is seeking candidates for several funded projects at the master’s and doctoral levels starting in the summer and fall of 2024. The Canada Research Chair in Software Specification, Testing, and Verification provides funding for students in the form of a scholarship for the duration of the project (2 years for M.Sc., 3 years for Ph.D.).

Proposed Projects

Click on the links below for a more detailed description of each project.

  • LIF24-M1: Monitoring a video game economy. Aims to use the machinations.io simulator to model the economy of video games, simulate scenarios to balance their difficulty, and export the data for analysis and transformation with the BeepBeep library.
  • LIF24-D1: Test and verification for event stream processing . Aims to develop theory, techniques, and tools for testing and formal verification of stream programs, particularly for processing pipelines in APIs like BeepBeep.
  • LIF24-D2: Evaluation of clinical skills through monitoring and ‘log analysis.Aims to formalize, implement, and evaluate the mechanisms for measuring the clinical skills of nurses by analyzing their actions in a game, using log analysis techniques and formal methods to produce explainable indicators for continuous improvement.
  • LIF24-D3: Detection of anomalies in a query system identity. Aims to analyze identity query logs in real time in a secure blockchain-based system to detect anomalies and suspicious behavior, using linear temporal logic and epistemic modal logic for formal modeling and practical verification via a monitor or smart contract.
  • LIF24-D4: Monitoring the project management of a video game by analyzing log files. Aims to develop automatic methods for processing log files in video game development, in order to generate alerts to prevent problems and assess project health, as well as to automatically identify and adjust necessary logging items.< /li>

Individuals wishing to apply are invited to fill out the online form at https://zfrmz.com/BGLMrz4QFYzkIOZxVtpD?lang=en providing the requested information.

Institution and Hosting Lab Presentation

The Université du Québec à Chicoutimi (UQAC) is part of Canada’s largest university network. It is located in the French-speaking region of Saguenay–Lac-Saint-Jean, renowned for the beauty of its fjord and the majesty of its surrounding nature. UQAC welcomes 6,500 students each year, including more than 1,000 from 50 different countries. The computer science research program is particularly dynamic; it hosts two Canada Research Chairs, currently includes about twenty professors, 30 doctoral and postdoctoral fellows, and more than 100 master’s students.

The doctoral work will take place at the Formal Computing Laboratory, under the supervision of Prof. Sylvain Hallé, holder of the Canada Research Chair on testing, specification, and verification of computer systems. The LIF specializes in the application of formal methods to testing and verification of various software systems. Previous projects by LIF faculty members have been conducted in collaboration with numerous companies, including Ericsson, Industrial Alliance, Ubisoft LaForge, Devicom, and Eckinox Media.

Research at LIF is internationally recognized and contributes to the development of concrete, high-quality software tools based on solid mathematical foundations. Notable long-standing projects developed at LIF include the BeepBeep 3 event stream processing engine [2], the Artichoke blockchain monitoring system [3], and the Petit Poucet data lineage library [4]. All these initiatives have been awarded and published in leading international conferences over the last decade.

References

  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
Tags: ,
Top

Discover more from LIF

Subscribe now to keep reading and get access to the full archive.

Continue reading