Abstract
With the advent of Information and Communication Technologies in recent decades, organizations face several challenges today. Adopting Digital Transformation (DT) offers numerous opportunities for Small and Medium Enterprises (SMEs) to improve their efficiency and operations, reaching new markets, shareholders, and customers. However, there are potential risks associated with this process. With Digital Transformation (DT), the radius of connectivity and interconnection between devices and systems increases in Mozambique and worldwide, creating more significant space cyberattacks. As Small and Medium-sized Enterprises (SMEs) connect to the digital world and move forward with adopting innovative digital technologies, they become more vulnerable to digital security risks. Hence, managing digital security risks effectively is crucial to realizing the benefits of Digital Transformation (DT). This position paper proposes to present the research work that will culminate in the proposal to develop a framework that fits Mozambican Small and Medium Enterprises (SMEs) through a Design Science Research (DSR) methodology, which can help to assist Mozambican Small and Medium Enterprises (SMEs) in the Digital Transformation (DT) process. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2026.

Abstract
Debugging and repairing faults when programs fail to formally verify can be complex and time-consuming. Automated Program Repair (APR) can ease this burden by automatically identifying and fixing faults. However, traditional APR techniques often rely on test suites for validation, but these may not capture all possible scenarios. In contrast, formal specifications provide strong correctness criteria, enabling more effective automated repair. In this paper, we present an APR tool for Dafny, a verification-aware programming language that uses formal specifications - including preconditions, post-conditions, and invariants - as oracles for fault localization and repair. Assuming the correctness of the specifications and focusing on arithmetic bugs, we localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program, and applying Large Language Models (LLMs) to synthesize candidate fixes. The models considered are GPT-4o mini, Llama 3, Mistral 7B, and Llemma 7B. We evaluate our approach using DafnyBench, a benchmark of realworld Dafny programs. Our tool achieves 89.7% fault localization success rate and GPT-4o mini yields the highest repair success rate of 74.18%. These results highlight the potential of combining formal reasoning with LLM-based program synthesis for automated program repair.

Abstract
Seaport cranes operate continuously and consume large amounts of energy while aiming to minimise containerships' berthing time. Although previous studies have contributed to addressing the crane scheduling problem, most have focused exclusively on loading time, often overlooking the aspect of energy consumption. Furthermore, crane activity is typically modelled in a simplified manner-commonly assuming a fixed cycle duration or constant energy usage when handling a container-without accounting for the impact of variable container masses. In this study, an energy-aware quay crane scheduling formulation for container terminals is proposed, highlighting the importance of integrating an energy model into the scheduling problem. The optimisation problem is formulated as a Mixed Integer Linear Programming (MILP) model. The objective is to minimise total energy costs by reordering the sequence in which containers are handled, while respecting precedence constraints defined by the ship's stowage plan. Two solution methods-a MILP approach solved using CPLEX and a genetic algorithm (GA)-are compared. The results indicate that, for larger containerships, the genetic algorithm provides a more efficient solution method. Moreover, incorporating detailed energy consumption models for electric cranes may significantly reduce energy costs during containership handling operations.

Abstract
This project was developed to improve the cost estimation process of new products within the Product Development Department of a furniture manufacturer. This work involved developing a methodology using Machine Learning (ML) models trained on products' existing data to predict the cost of new innovative ones based on similarities and given data. The ML models used were Linear Regression (LR), Light Gradient-Boosting Machine (LGBM), Random Forest (RF), and Support Vector Machine (SVM). The proposed methodology considers the estimation of the total cost of producing a product, which encompasses both material and operational costs. Throughout this project, several analyses were developed to identify and evaluate different independent variables that could explain the behaviour of these two cost components. The suitability of the different variables was studied by applying several ML models, and a set of functions that return an estimate of the cost as a function of these predictor variables was obtained. The proposed approach, which incorporates ML models into more complex variables to predict, resulted in a 19.29% reduction in estimation error.

Abstract
Despite the recognised potential of horizontal collaboration in logistics to reduce inefficiencies, and the increasing academic interest in this topic, in practice many initiatives fail. One of the main reasons for this failure is the poor strategy planning and governance organisation. This paper addresses this gap proposing a comprehensive conceptual framework to support the design and implementation of a common strategy for the stakeholders of such partnerships. The research employs qualitative methods, drawing on interviews and the case analysis of existent initiatives. The proposed framework involves the main phases of the strategic formulation, deciding the stakeholder engagement, strategic formulation, operational implementation, and business model elaboration. It serves as a road map for stakeholders to avoid common mistakes and accelerate the deployment of cooperative partnerships.

Abstract
Students in computing education increasingly use large language models (LLMs) such as ChatGPT. Yet, the role of LLMs in supporting cognitively demanding tasks, like deductive program verification, remains poorly understood. This paper investigates how students interact with an LLM when solving formal verification exercises in Dafny, a language that supports functional correctness by allowing programmers to write formal specifications and automatically verifying that the implementation satisfies the specification. We conducted a mixed-methods study with master's students enrolled in a formal methods course. Each participant completed two verification problems, one with access to a custom ChatGPT interface that logged all interactions and the other without. We identified strategies used by successful students and assessed the level of trust students place in LLMs. Our findings show that students perform significantly better when using ChatGPT; however, performance gains are tied to prompt quality. We conclude with practical recommendations for integrating LLMs into formal methods courses more effectively, including designing LLM-aware challenges that promote learning.