Abstract
With technological advancements, much data is being captured by sensors, smartphones, wearable devices, and so forth. These vast datasets are stored in data centres and utilized to forge data-driven models for the condition monitoring of infrastructures and systems through future data mining tasks. However, these datasets often surpass the processing capabilities of traditional information systems and methodologies due to their significant size. Additionally, not all samples within these datasets contribute valuable information during the model training phase, leading to inefficiencies. The processing and training of Machine Learning algorithms become time-consuming, and storing all the data demands excessive space, contributing to the Big Data challenge. In this paper, we propose two novel techniques to reduce large time-series datasets into more compact versions without undermining the predictive performance of the resulting models. These methods also aim to decrease the time required for training the models and the storage space needed for the condensed datasets. We evaluated our techniques on five public datasets, employing three Machine Learning algorithms: Holt-Winters, SARIMA, and LSTM. The outcomes indicate that for most of the datasets examined, our techniques maintain, and in several instances enhance, the forecasting accuracy of the models. Moreover, we significantly reduced the time required to train the Machine Learning algorithms employed.

Abstract
The connection of distributed energy resources in distribution system have been increasing significantly, requiring new approaches as market-based flexibility solutions. This paper proposes the coordinated operation of on-load tap changer and flexibility services traded in a local market for voltage regulation in medium and low voltage grid. The wider action of on-load tap changer is used to restore voltages at the medium voltage feeder based on sensitivity coefficients. If voltage violations persist, flexibilities are traded in a local energy market with a cost-effective approach, where flexibility costs are minimized, and are activated according to their effectiveness indicated by sensitivity coefficients. Sensitivity coefficients are obtained in the medium voltage using an analytical approach that can be applied to multi-phase unbalanced systems, and in the low voltage using a data-driven approach due to their limited observability. Results show the proposed approach can be an effective solution to regulate voltages, combining the wider action of on-load tap changer with local flexibility, avoiding unnecessary tap changes and requesting a small volume of flexibility services. © 1972-2012 IEEE.

Abstract
The increasing occurrence of extreme weather events has severely compromised the resilience of power distribution systems, resulting in widespread outages and substantial economic losses. This paper proposes a novel solution to enhance the resilience of distribution networks without the need for significant infrastructure upgrades. We introduce a bilevel optimization framework that integrates Demand Response Programs (DRPs) to strategically manage electricity consumption and mitigate the impact of system disruptions. The approach fosters collaboration between Distribution System Operators (DSOs) and Demand Response Aggregators (DRAs), optimizing both operational resilience and economic efficiency. To solve the bilevel problem, we employ a Mathematical Program with Equilibrium Constraints (MPEC), transforming the bilevel model into a single- level problem by utilizing the Karush-Kuhn-Tucker (KKT) conditions. This method is applicable when the lower-level problem is convex with linear constraints. The model also incorporates Long Short-Term Memory (LSTM) neural networks for wind generation forecasting, enhancing decision-making precision. Furthermore, we conduct multiple case studies under varying severities of incidents to evaluate the method's effectiveness. Simulations performed on the IEEE 33-bus test system using GAMS and Python validate that the proposed method not only improves system resilience but also encourages active consumer participation, making it a robust solution for modern smart grid applications. The simulation results show that by performing DRP to handle the contingencies in a high-impact incident, the resilience of the system can be improved by 5.3%.

Abstract
This paper addresses a job shop scheduling problem with peak power constraints, in which jobs can be processed once or multiple times on either all or a subset of the machines. The latter characteristic provides additional flexibility, nowadays present in many manufacturing systems. The problem is complicated by the need to determine both the operation sequence and starting time as well as the speed at which machines process each operation. Due to the adherence to renewable energy production and its intermittent nature, manufacturing companies need to adopt power-flexible production schedules. The proposed power control strategies, that is, adjusting processing speed and timing to reduce peak power requirements may impact production time (makespan) and energy consumption. Therefore, we propose a bi-objective approach that minimizes both objectives. A linear programming model is developed to provide a formal statement of the problem, which is solved to optimality for small-sized instances. We also proposed a multi-objective biased random key genetic algorithm framework that evolves several populations in parallel. Computational experiments provide decision and policymakers with insights into the implications of imposing or negotiating power consumption limits. Finally, the several trade-off solutions obtained show that as the power limit is lowered, the makespan increases at an increasing rate and a similar trend is observed in energy consumption but only for very small makespan values. Furthermore, peak power demand reductions of about 25% have a limited impact on the minimum makespan value (4-6% increase), while at the same time allowing for a small reduction in energy consumption.

Abstract
Digital marketing has become an integral part of the modern business landscape, revolutionizing the way companies promote their products and interact with their customers. In this essay, we aim to demonstrate how it can be related to an increased tendency for mental health problems and other societal complications, as well as developing insights into its evolution using the latest breakthroughs in technology. This study will provide an overview of the impacts of digital marketing on companies, and in society, resorting to classical literature, as well as recent studies and articles conducted on the matter. An online survey was developed to support our research, reaching 112 Portuguese participants. The scientific methodology used was the Chi-Square test, with a confidence margin of 95% targeting two focus groups, one with their ages comprised within 16-25 years old and the other from 35 to 50 years old. We perceived that there would be behavioral differences between people who were born in the digital marketing age and those who had to adapt to it. We also provided some possible solutions to the problems raised by digital marketing and explained how these issues could be exacerbated with the renaissance technology is facing recently.

Abstract
Jasmin is a programming language for high-speed and high-assurance cryptography. Correctness proofs of Jasmin programs are typically carried out deductively in EasyCrypt. This allows generality, modularity and composable reasoning, but does not scale well for low-level architecture-specific routines. CryptoLine offers a semi-automatic approach to formally verify algebraically-rich low-level cryptographic routines. CryptoLine proofs are self-contained: they are not integrated into higher-level formal verification developments. This paper shows how to soundly use CryptoLine to discharge subgoals in functional correctness proofs for complex Jasmin programs. We extend Jasmin with annotations and provide an automatic translation into a CryptoLine model, where most complex transformations are certified. We also formalize and implement the automatic extraction of the semantics of a CryptoLine proof to EasyCrypt. Our motivating use-case is the X-Wing hybrid KEM, for which we present the first formally verified implementation. © 2025 Copyright held by the owner/author(s).