Students wanted for several master’s and doctoral projects

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