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
Immunohistochemistry (IHC) is crucial for the clinical categorisation of breast cancer cases. Deep generative models may offer a cost-effective alternative by virtually generating IHC images from hematoxylin and eosin samples. This review explores the state-of-the-art in virtual staining for breast cancer biomarkers (HER2, PgR, ER and Ki-67) and benchmarks several models on public datasets. It serves as a resource for researchers and clinicians interested in applying or developing virtual staining techniques.

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.

Abstract
E-commerce growth is driving the need for novel, more sustainable last-mile delivery strategies. One potential strategy is based on setting up a mobile-depot from where last-mile deliveries are conducted using cargo bikes. This research explores the impacts of this strategy through a microscopic traffic simulation based on a medium-sized European city. The strategy was evaluated at three levels: operational (route length and duration), energy consumption, and emissions. The results showed that adopting a last-mile delivery strategy based on a mobiledepot and cargo bikes leads to significant benefits in terms of energy consumption and emission, which decrease by more than 80 %, but imply lengthier (+49 %) and more time-consuming (+14 %) routes compared to a traditional parcel delivery strategy.

Abstract
Corporate Social Responsibility (CSR) is increasingly shaping the pathways of Small Medium-sized Enterprises (SMEs). This study presents an entity-relationship diagram (ERD) approach to 184 determinants of SME internationalization success, in order to provide structured inputs for Deep Learning (DL) Recommenders that can support CSR-aligned internationalization strategies. Employing Visual Paradigm 17.2 Professional software for modeling, the research synthesizes state-of-the-art findings on foreign market entry, and export performance, into ERDs. Then the market adoption drivers for such a DL tool are explored through semi-structured interviews with twelve stakeholders. The results reveal a propensity to adopt the DL recommender, with experts highlighting essential features for engagement, pricing, and implementation. The discussion contextualizes these findings, while the conclusion addresses gaps and future directions. The study's focus in Portugal/Germany may limit worldwide extrapolation, yet it advances knowledge by consolidating success determinants, validating platform requirements, exposing gaps, and suggesting research in both CSR, AI and SME internationalization.