Here you will discover a compilation of currently available Bachelor and Master thesis opportunities, as well as internships. Additionally, there might be fresh projects to explore, so feel free to inquire if any catch your interest.
Guidelines for Pursuing an Internship or Thesis Collaboration
- Time Management: crafting a quality bachelor thesis typically demands approximately three months, while a Master's thesis can extend to six months or more. Feel free to express interest in topics beforehand, even if your exams aren't yet completed. If any topics listed here intrigue you, don't hesitate to mention it upfront.
- Communication Efficiency: when updating on your progress, sending only one email per month is insufficient, while sending one email per day is excessive. Strive for efficiency in both the content and frequency of your communications.
- Detailed Reporting: avoid the vague "it doesn't work" approach. Provide clear explanations of attempted solutions and the specific circumstances surrounding any encountered issues. Proactivity and clarity are key.
- Writing Standards: embrace LaTeX for document creation, a skill that may initially seem daunting but offers substantial benefits as you progress. Overleaf serves as an excellent platform for collaborative work.
- Personal Responsibility: the internship or thesis endeavor rests squarely on your shoulders. Remembering deadlines, paperwork, and administrative tasks falls within your domain; I won't issue reminders.
Available Theses
Note that the list is incomplete. If you are interested in any of the following topics, please contact me to discuss possible additional theses further:
- Multi-Agent Systems (MAS)
- Formal Verification
- Robotics
- Chatbots
- Process Mining
- Automated Planning
- Reinforcement Learning
- Agent-Based Modeling and Simulation
| Bachelor/Master | Title | Abstract | Partners | Topics |
|---|---|---|---|---|
| Formal Verification | ||||
| Bachelor/Master | Combination of Runtime Verification and Nudging | The project focuses on integrating Runtime Verification (RV) with the concept of Nudging to enhance the reliability and user interaction of software systems. Runtime Verification is a method that monitors a system's execution in real-time to ensure it adheres to specific behaviors or properties. This technique is crucial in safety-critical systems, where any deviation from expected behavior can have serious consequences. However, while RV is effective in identifying these deviations, it does not typically influence the user's decisions or actions. Nudging, a concept from behavioral economics, subtly guides users towards making better decisions without restricting their freedom of choice. The goal of this thesis is to explore how these two approaches can be combined to create systems that not only monitor for correct behavior but also encourage users to make decisions that align with safety and performance goals. The project will involve designing and evaluating a framework that integrates Nudging into RV, with the potential to improve both system reliability and user experience. This research offers the opportunity to contribute to the development of more robust and user-friendly software systems. | Runtime Verification / AI | |
| Bachelor/Master | GUI support for formal verification tool VITAMIN | The VITAMIN formal verification framework is a sophisticated tool used for ensuring the correctness of system models through rigorous formal methods. However, its current text-based interface poses a significant barrier to entry for users who are not well-versed in formal verification syntax and methodologies. This project aims to develop a graphical user interface (GUI) for VITAMIN, providing a more accessible and intuitive way for users to create and manipulate verification models. The proposed GUI will support drag-and-drop functionality, allowing users to visually construct and modify models without needing to write complex code. This approach not only lowers the learning curve but also enhances productivity by making the model creation process more straightforward and less error-prone. The development of this GUI will involve designing an interactive and visually appealing interface that integrates seamlessly with VITAMIN's underlying framework. By enabling users to draw models through simple drag-and-drop actions, the GUI will transform the user experience, making formal verification more approachable and efficient. The final deliverable will be a robust, user-friendly GUI that empowers users to leverage the full capabilities of VITAMIN without the need for extensive technical expertise in formal verification. This advancement is expected to broaden the adoption of formal verification practices and improve the overall quality and reliability of system models across various domains. | Vadim Malvone, Telecom Paris | Formal Verification / Software development |
| Bachelor/Master | Machine Learning for Optimal Metric Selection in LTL Runtime Verification | Linear Temporal Logic (LTL) is crucial in runtime verification, where a monitor checks system properties against LTL specifications. Due to resource constraints, the monitor must selectively observe certain atoms (propositions) based on a metric that evaluates their potential payoff. Current metrics are often manually defined, which may not be optimal across varying scenarios. This thesis aims to apply machine learning (ML) techniques to learn the best metric for atom selection in runtime LTL verification. By analyzing example traces of system executions, the project will train an ML model to predict the most effective metric, optimizing the verification process under resource constraints. The project involves analyzing existing metrics, curating a dataset of system traces, and exploring ML algorithms to identify the most suitable approach. The developed model will be tested within a runtime verification framework to compare its performance against traditional methods. The expected outcome is a learned metric that enhances the accuracy and efficiency of runtime verification, particularly in resource-limited environments. | Vadim Malvone, Telecom Paris | Formal Verification / Machine Learning |
| Bachelor/Master | Genetic Algorithms for learning properties | This thesis explores the application of genetic algorithms (GAs) in learning formal properties. It investigates how GAs can efficiently navigate complex search spaces to uncover and represent formal properties, offering insights into their effectiveness and limitations. The study aims to contribute to the understanding of utilizing GAs for learning formal properties, providing valuable implications for various domains, including artificial intelligence, optimization, and robotics. | Formal Verification / AI | |
| Bachelor/Master | Formal Verification of Large Language Models: A Case Study on ChatGPT | Large Language Models (LLMs) like OpenAI's ChatGPT have revolutionized natural language processing, providing human-like text generation for various applications. Despite their impressive performance, ensuring their reliability, safety, and correctness remains a significant challenge. Formal verification, a method used to prove the correctness of systems through mathematical techniques, presents a potential solution. This thesis proposes to apply formal verification techniques to LLMs, specifically focusing on ChatGPT. The primary objectives are to define formal specifications for ChatGPT, develop verification techniques suitable for LLMs, and implement and evaluate verification tools. Initially, a thorough literature review will be conducted to understand existing formal verification techniques and their application to AI systems. This research is expected to contribute significantly to the field by providing a set of formal specifications for LLMs, developing novel verification algorithms, and creating practical verification tools. The case studies will offer valuable insights into the effectiveness of formal verification techniques in real-world applications of ChatGPT. | Formal Verification / Natural Language Processing | |
| Bachelor/Master | Extending the Runtime Monitoring Language (RML) to Support Metric Time Specification | The Runtime Monitoring Language is a versatile formalism for representing complex rules but lacks support for precise temporal reasoning. This thesis proposes extending RML with metric time specifications, akin to those in Metric Temporal Logic (MTL), enabling the use of time intervals and windows within rules. This enhancement will make RML more suitable for applications requiring exact timing constraints, such as event scheduling and monitoring systems. More information on RML can be found at RMLatDIBRIS. The primary objectives are to integrate metric time intervals into RML, define formal semantics for these extensions, and develop a prototype system to demonstrate their practical utility. The methodology involves designing the syntax and semantics for the extended RML, implementing a prototype, and evaluating its performance using real-world scenarios. This evaluation will measure the system's expressiveness, computational efficiency, and practical applicability. The extended RML will offer enhanced expressiveness for temporal reasoning, supported by formal semantics and demonstrated through a prototype system. This research will provide empirical evidence of the benefits and limitations of incorporating metric time specifications into RML, potentially expanding its use in various domains requiring precise temporal logic. | Davide Ancona, University of Genova | Runtime Verification |
| Bachelor/Master | A Study of State-of-the-Art Runtime Verification Techniques in AI | The increasing complexity and autonomy of Artificial Intelligence (AI) systems, especially in critical applications such as healthcare, autonomous driving, and financial services, necessitates robust methods to ensure their reliability and safety. Runtime Verification (RV) has emerged as a promising technique to provide these assurances by continuously monitoring system behavior against formal specifications during execution. This thesis proposes to conduct a comprehensive study of the state-of-the-art RV techniques applied to AI systems, evaluating their effectiveness, scalability, and practicality. The primary objective of this research is to systematically review and classify existing RV techniques used in AI, highlighting their strengths, limitations, and areas for improvement. The study will cover various AI domains, including machine learning models, neural networks, and autonomous decision-making systems. We will analyze how current RV methods handle challenges such as non-deterministic behavior, high-dimensional data, and the dynamic nature of learning algorithms. Additionally, we will explore the integration of RV with AI development frameworks to enhance real-time monitoring and anomaly detection capabilities. This research will contribute to the field by providing a detailed taxonomy of RV techniques in AI, identifying gaps in current approaches, and proposing future research directions. By evaluating and comparing these techniques, we aim to offer valuable insights for researchers and practitioners seeking to implement effective runtime verification in AI systems, ultimately contributing to the development of safer and more reliable AI technologies. | Christian Colombo, University of Malta | Runtime Verification |
| Bachelor/Master | Runtime Monitoring of IoT Wearable Devices in Healthcare for Diabetes Management | The growing use of wearable IoT devices in healthcare, particularly for managing chronic conditions such as diabetes, has introduced new opportunities for real-time health monitoring. Devices like continuous glucose monitors (CGMs) and smartwatches are used to track essential health metrics such as blood glucose levels and heart rate, providing critical data to patients and healthcare providers. These wearables are especially important for diabetic patients, as they offer real-time information to guide decisions regarding insulin administration, diet, and physical activity. However, the safety-critical nature of healthcare applications makes it essential to ensure that these devices behave as expected at all times. Any malfunction or inaccurate data can lead to serious health risks, such as hypoglycemia or hyperglycemia, which may result in life-threatening consequences. Despite the importance of these devices, there is currently a lack of robust systems for monitoring their real-time performance and ensuring their correct behavior during operation. This research proposes the development of a runtime monitoring framework specifically designed for wearable devices used in diabetes management. The goal is to continuously track the performance of these devices, detect anomalies or deviations from expected behavior, and ensure the accuracy and reliability of the data they produce. By monitoring these devices in real time, the system would be able to alert users and healthcare providers of any malfunctions, ensuring timely interventions and reducing the risk of adverse health events. The research will involve the analysis of real-world data from diabetic patients using wearables, the design and implementation of the monitoring framework, and the evaluation of its effectiveness in detecting device errors and improving reliability. The expected outcome is a reliable monitoring solution that enhances the safety of wearable healthcare devices, ensuring that patients can rely on the information they provide for managing their condition effectively. | Giorgio Delzanno, University of Genova | Runtime Verification / IoT |
| Multi-Agent Systems | ||||
| Bachelor/Master | SimJade: Simulating Jade Platform sas p2p nodes | A Multi-agent system (MAS) is a software where many autonomous and proactive entities (the agents) can collaborate to solve complex tasks. A MAS is a particular type of distributed system, where the involved entities are logically distributed, and often physically distributed too. Many MAS development frameworks exist, among them JADE is one of the mostly adopted in academia and in industry too: it is a Java based framework supporting the developers in creating the MAS, and offers support to make the agents communicate in a transparent way even if they are running on different physical machines. Anyway, two JADE platforms can communicate only if they know their IPs. When testing such logically and distributed MASs before the deployment, we should need many physical machines to replicate the final deployment, or being able to manage many virtual machines, and all the complexity related to the network management: this make this testing setup extremely expensive and usually unrealistic to be available, preventing the MAS to be concretely and extensively tested. The aim of this thesis is the refactoring, design and systematic testing of SimJADE, a prototype of a simulator able to run on a single machine many JADE Platforms, so that to support the testing of a JADE MAS in a simulated distributed scenario without any change in the original MAS’ code. SimJADE is currently developed starting from PeerSim (a p2p simulator) and JADE, but some important aspects of JADE still need to be integrated in it, and some important aspects of the simulation need to be studied and integrated in the tool. The student will be asked to study how these missing aspects can be modeled and implemented in SimJade, so that to improve the simulator. Then, a set of MASs need to be found in literature and used to extensively test the simulator, so that to verify its capabilities and limitations. The thesis integrates Software Engineering and MAS design skills and approaches, and foresees both a detailed design analysis and an implementation phase. | Daniela Briola, University of Insubria | Multi-Agent Systems |
| Bachelor/Master | Runtime Verification in MESA | "Mesa is a well-adopted open source agent-based modeling (ABM) framework built in Python 3 and published under an Apache 2.0 license and the only agent-based modeling library that is NUMFOCUS affiliated. The goal of Mesa is to be easy to use, as well as easily integrated into the Python ecosystem. Mesa provides tools that allow parameter sweeps, in-browser visualizations, remote hosting, headless model runs, and an architecture that decouples design components. Mesa also integrates things like network analysis and geospatial modeling and allows for members of the ecosystem to build and contribute back libraries that extend the functionality of Mesa both generally as well as specifically to the domain in which the contributor is an expert. The aim of this thesis is to develop a Runtime Verification library to integrate in Mesa. The objective is to give the possibility to enhance the simulations with formal verification features. In particular, to let the developer add requirements and constraints to be met by the agent-based simulation. The student will be asked to develop such library and to validate its use on some existent simulation example." | Multi-Agent Systems / Agent-Based Modeling and Simulation | |
| Bachelor/Master | Comparative Analysis of Symbolic and Sub-Symbolic Agents in Collaborative Multi-Agent Environments using Overcooked-AI | This thesis proposes a comparative analysis of symbolic and sub-symbolic agents using the Overcooked-AI environment, available at Overcooked-AI GitHub. The goal is to develop rule-based symbolic agents and benchmark their performance against deep learning-based sub-symbolic agents in collaborative cooking tasks. By leveraging the structured, interpretable nature of symbolic AI and the adaptive, data-driven capabilities of sub-symbolic AI, this study aims to uncover their respective strengths and weaknesses in complex, dynamic settings. The research will focus on key metrics such as task completion time, cooperation efficiency, and adaptability to changing scenarios. By conducting extensive experiments within the Overcooked-AI framework, we will analyze differences in strategy and behavior between the two types of agents. Additionally, the thesis will explore hybrid approaches that integrate symbolic reasoning into sub-symbolic frameworks, potentially combining the interpretability of symbolic methods with the adaptability of sub-symbolic techniques. The findings are expected to provide valuable insights into the design of AI agents for cooperative tasks, highlighting the potential for synergistic approaches that leverage the best of both paradigms. | Rafael C. Cardoso, University of Aberdeen | Multi-Agent Systems / Machine Learning |
| Security | ||||
| Bachelor/Master | Securing Robot-Collected Digital Evidence | Robots are involved in military operations and rescue missions which frequently involve evidence collection. As such, robots may be carrying sensitive information which need to be protected for privacy, while strictly maintaining a chain of custody such that the evidence is admissible in a court of law. Focusing on the first part, this project explores how an RV-TEE [1] can be adopted to protect sensitive data while it is in the robot’s custody: RV-TEE is an architecture which prescribes a combination of software and hardware to protect the execution of cryptographic operations and safely store the related keys. At its core, RV-TEE uses a hardware security module (HSM) to provide isolation and protection from a number of side-channel attacks. The software component is based on runtime verification techniques which monitor the interaction of the HSM with the rest of the robot components and environment. Acting as a gatekeeper, such monitoring ensures that the access to the HSM-hosted functionality strictly adheres to a limited sequence of operations, whose parameters are also vetted for further restriction of the attack surface. While the above concept is generic, this project explores an instantiation with the Robot Operating System (ROS, https://www.ros.org/) ecosystem, employing the SECube chip (https://www.secube.blu5group.com/) as an HSM, and ROSMonitoring [2] framework instantiated with Larva [3] as the RV component. [1] RV-TEE: Secure Cryptographic Protocol Execution based on Runtime Verification, Mark Vella, Christian Colombo, Robert Abela, and Peter Špaček, Journal of Computer Virology and Hacking Techniques, 2021. [2] ROSMonitoring: A Runtime Verification Framework for ROS, Angelo Ferrando, Rafael C. Cardoso, Michael Fisher, Davide Ancona, Luca Franceschini, Viviana Mascardi, in TAROS 2020, Nottingham, UK. [3] LARVA - Safer Monitoring of Real-Time Java Programs, Christian Colombo, Gordon J. Pace and Gerardo Schneider, in SEFM 2009, Hanoi, Vietnam. | Christian Colombo, University of Malta | Security |
| Bachelor/Master | Monitor code attestation | Runtime monitors frequently need to be deployed in highly secure software environments to help further secure the system under scrutiny. In such contexts, the monitor could benefit from security hardening over and above the rest of the system since the monitoring component is of particular interest to the attacker. If the attacker successfully disables the monitor, the attack can be executed without potential alarms being raised, leaving no evidence behind. Furthermore, due to separation of concerns inherent in runtime verification, monitors are typically separated from the rest of the system, facilitating isolation and a hardened security environment which would otherwise be difficult to achieve for the whole system. Through our paper [AREA23] we have explored two threat models and corresponding efforts to protect against them. In subsequent work, we have continued to expand this model into a comprehensive security stack called RVsec. This project aims to expand the current implementation of the RVsec stack, particularly the monitor code attestation component. Once implemented, this component ensures that the monitoring code is not compromised, i.e., its signature is checked regularly for consistency. Evaluating the implementation involves checking the overhead introduced and simulating attacks to check for effectiveness. [AREA23] Robert Abela, Christian Colombo, Axel Curmi, Mattea Fenech, Mark Vella, Angelo Ferrando: Runtime Verification for Trustworthy Computing. AREA@ECAI 2023: 49-62 |
Christian Colombo, University of Malta | Runtime Verification / Security |
| Bachelor/Master | Attack Simulation | This project builds on previous work from multiple research groups in attack modelling and simulation. The final objective is to come up with a framework to model and simulate attacks on infrastructure using a combination of system modelling and network simulation techniques. The framework should be able to verify the feasibility of a particular attack, in terms of pre-defined security requirements which should be stated by means of temporal logic (LTL, MITL). Once a system is modelled within a particular network topology, the goal is to simulate all possible attacks (similar to model checking) and provide a trace of how an attacker might compromise the system, which components will be affected and when. The output of such a framework should assist security officers in better understanding where the vulnerabilities are and how attacks can be prevented. This project requires a background in model checking and a basic understanding of how networking protocols operate. Knowledge in RV would also be very useful. Familiarity with popular model checkers (e.g. Spin, Uppaal) and network simulators (e.g. NS2, Mininet) would be ideal. | Christian Colombo, University of Malta | Runtime Verification / Security |
| Bachelor/Master | Suitable Case Study for RVsec | Runtime monitors frequently need to be deployed in highly secure software environments to help further secure the system under scrutiny. In such contexts, the monitor could benefit from security hardening over and above the rest of the system since the monitoring component is of particular interest to the attacker. If the attacker successfully disables the monitor, the attack can be executed without potential alarms being raised, leaving no evidence behind. Furthermore, due to separation of concerns inherent in runtime verification, monitors are typically separated from the rest of the system, facilitating isolation and a hardened security environment which would otherwise be difficult to achieve for the whole system. Through our paper [AREA23] we have explored two threat models and corresponding efforts to protect against them. In subsequent work, we have continued to expand this model into a comprehensive security stack called RVsec. So far, RVsec has been instantiated on a Quantum-safe security protocol implementation in the context of a chat application. While results are encouraging, the approach needs further validation through further case studies. This project aims to explore a substantially different case study, potentially from the area of robotics to assess the applicability of RVsec. [AREA23] Robert Abela, Christian Colombo, Axel Curmi, Mattea Fenech, Mark Vella, Angelo Ferrando: Runtime Verification for Trustworthy Computing. AREA@ECAI 2023: 49-62 |
Christian Colombo, University of Malta | Runtime Verification / Security |
| Bachelor/Master | Extending RVsec with Performance and Security Properties | Runtime monitors frequently need to be deployed in highly secure software environments to help further secure the system under scrutiny. In such contexts, the monitor could benefit from security hardening over and above the rest of the system since the monitoring component is of particular interest to the attacker. If the attacker successfully disables the monitor, the attack can be executed without potential alarms being raised, leaving no evidence behind. Furthermore, due to separation of concerns inherent in runtime verification, monitors are typically separated from the rest of the system, facilitating isolation and a hardened security environment which would otherwise be difficult to achieve for the whole system. Through our paper [AREA23] we have explored two threat models and corresponding efforts to protect against them. In subsequent work, we have continued to expand this model into a comprehensive security stack called RVsec. RVsec comprises two kinds of RV monitors: functional monitors and performance/security monitors. While functional monitors are usually specific for a particular application, performance and security monitors could be more generic, focusing also on relevant signals coming from the host machine. For example, one could observe a period of heightened volume of traffic, use of commands like “whoami” (used by attackers for reconnaissance), brute forcing of logins or “su” (used for privilege escalation), service set up running as admin/root (used for persistence). Such observable behaviour can be encoded in terms of RV properties to warn of ongoing attacks being sustained by the system. The outcome of this project involves the identification of such properties and their incorporation into the RVsec stack as monitors. A case study would then serve as validation of the approach and to measure the overheads introduced. [AREA23] Robert Abela, Christian Colombo, Axel Curmi, Mattea Fenech, Mark Vella, Angelo Ferrando: Runtime Verification for Trustworthy Computing. AREA@ECAI 2023: 49-62 |
Christian Colombo, University of Malta | Runtime Verification / Security |
| Robotics | ||||
| Bachelor/Master | Extending and Applying ROSMonitoring Framework for Robotic Systems | ROSMonitoring provides a robust framework for monitoring and verifying robotic systems. This thesis proposes to broaden its capabilities and apply it across various domains within robotics. The primary objectives are twofold: first, to enhance ROSMonitoring through the integration of new features that bolster its monitoring and verification functionalities, and second, to apply ROSMonitoring in diverse robotic domains to assess its efficacy and versatility. Extending and applying the ROSMonitoring framework holds promise for advancing monitoring and verification practices in robotics. By systematically enhancing the framework's capabilities and exploring its application in diverse contexts, this thesis aims to contribute significantly to the field of robotics research and development. | Runtime Verification / Robotics | |
| Bachelor/Master | Integration of LARVA and ROSMonitoring for Enhanced Runtime Verification in Robotic Systems | This thesis proposal seeks to integrate two runtime verification tools, LARVA and ROSMonitoring, to improve the reliability and safety of robotic systems. LARVA, from the University of Malta, monitors Java programs to ensure they meet specified properties, while ROSMonitoring focuses on verifying ROS-based applications. The integration aims to create a comprehensive framework that leverages both tools' strengths for robust runtime verification in complex robotic systems. As robotic systems become more prevalent in critical applications like healthcare and autonomous vehicles, ensuring their reliability and safety is essential. Runtime verification provides guarantees about system behavior during execution by continuously checking it against formal specifications. LARVA is effective in monitoring Java programs, and ROSMonitoring verifies ROS topics to ensure message adherence to specified properties. The thesis's primary objective is to develop a unified runtime verification framework for ROS-based systems by integrating LARVA and ROSMonitoring. Specific goals include analyzing compatibility, developing an integration architecture, implementing the framework, and evaluating its performance on benchmark applications. The framework's efficacy in detecting and reporting real-time property violations will be demonstrated. | Christian Colombo, University of Malta | Runtime Verification / Robotics |
| Autonomous Vehicles | ||||
| Bachelor/Master | Formal Synthesis of Vehicle Modifications to Meet ODD Requirements in Autonomous Driving | The Operational Design Domain (ODD) defines the specific conditions and environments under which an autonomous vehicle (AV) can safely operate. Traditionally, determining the necessary modifications for a vehicle to meet ODD requirements has been a manual process, leading to inefficiencies and potential oversights. This thesis proposes a formal methods approach to automatically synthesize the minimal set of sensors, actuators, and system enhancements required for an AV to satisfy given ODD specifications. By inputting the ODD parameters into a formal synthesis framework, the system will generate recommendations for vehicle modifications that ensure compliance with the ODD. This research aims to streamline the vehicle adaptation process, reduce development time, and enhance the reliability of autonomous systems by providing a systematic method for aligning vehicle capabilities with operational requirements. | Formal Synthesis / Autonomous Vehicles | |
| Bachelor/Master | Formal Verification of Vehicle Compliance with Operational Design Domain Specifications | Verifying that an autonomous vehicle's existing configuration aligns with its intended Operational Design Domain (ODD) is crucial for safe and effective deployment. Current practices rely heavily on manual analysis to assess whether a vehicle's sensors, actuators, and control systems meet ODD requirements, which can be error-prone and inefficient. This thesis introduces a formal verification framework that takes both the ODD specifications and the vehicle's existing hardware and software configurations as inputs. By modeling these elements within a formal system, the framework will automatically verify compliance, identify discrepancies, and highlight areas needing enhancement. The goal of this research is to provide a rigorous, automated method for validating that an autonomous vehicle can operate safely within its designated ODD, thereby improving safety standards and reducing the risk of operational failures. | Formal Methods / Autonomous Vehicles | |