Abstract
This paper presents a semantic characterization of leakage-freeness through timing side-channels for Jasmin programs. Our characterization covers probabilistic Jasmin programs that are not constant-time. In addition, we provide a characterization in terms of probabilistic relational Hoare logic and prove the equivalence between both definitions. We also prove that our new characterizations are compositional and relate our new definitions to existing ones from prior work, which could only be applied to deterministic programs. To provide practical evidence, we use the Jasmin framework to develop a rejection sampling algorithm and provide an EasyCrypt proof that ensures the algorithm's implementation is leakage-free while not being constant-time.

Abstract
By connecting maritime and land transport, container terminals play a critical role in global logistics systems, as part of broader intermodal networks. The evolution of containerisation and technological advances, along with increased demand and volumes, led to significant adaptations in these terminals, as a way to improve productivity, reduce costs and increase competitiveness, while coping with spatial and operational constraints. For strategic decision-making, managing these complex systems can be enhanced by simulation models allowing the analysis of different scenarios in dynamic, uncertain environments. This work, presents a simulation-based decision support tool developed in the FlexSim software, to analyse different container terminal configurations, with a particular focus on automation and on sustainable practices to reduce the energy consumption of terminals. A discrete event simulation model was developed to study multiple scenarios impacting productivity, resource utilisation, and waiting times. The proposed approach allows the test and evaluation of management strategies for port operations, with preliminary results showing that sizing and planning of the fleets of automated guided vehicles (AGV) can significantly affect the total operating time, the energy consumed, and the costs associated with battery charging operations. Future research should explore additional factors affecting container terminal operations, such as the reorganisation of the storage area, while incorporating optimisation elements for work planning and resource allocation. Moreover, the simulation model will be tested and validated in a real case study, designed for the Port of Sines in Portugal. © 2024 The Authors.

Abstract
The development of safety-critical systems is heavily governed by domain-specific standards. In the aerospace industry, the DO-178C - Software Considerations in Airborne Systems and Equipment Certification - serves as the primary certification standard used by agencies such as the FAA and EASA to review and approve software-based systems. Although DO-178C aims to ensure system safety while providing evidence for certification, it does not prescribe a specific software development process, allowing flexibility for traditional Waterfall, Agile, or hybrid methods with appropriate adaptations for the aerospace context. This study proposes Scrum4DO178C, an Agile process based on Scrum, to meet the demanding requirements of aerospace software, including safety, robustness, reliability, and integrity. Scrum4DO178C introduces novel process enhancements specifically tailored to meet these criticality needs, while aligning with the standard. Unlike previous proposals that lack detail, this research presents a comprehensive, validated process applied in a real-world industry project at the highest criticality level (Level A - Catastrophic), offering insights beyond theoretical scenarios. The findings demonstrated that the Scrum4DO178C process improves project performance, allows frequent and manageable requirement changes, reduces Verification & Validation (V&V) effort, and increases efficiency while maintaining full compliance with DO-178C. The study also identifies areas for further improvement and suggests exploring the process in additional case studies, both within the aerospace industry and other domains with similarly stringent safety-critical requirements. Finally, it confirms that appropriate automation, namely for documentation production, is a central element to further improve the process. © 2013 IEEE.

Abstract
This paper describes an approach to algorithmic music composition that takes narrative structures as input, allowing composers to create music directly from narrative elements. Creating narrative development in music remains a challenging task in algorithmic composition. Our system addresses this by combining leitmotifs to represent characters, generative grammars for harmonic coherence, and evolutionary algorithms to align musical tension with narrative progression. The system operates at different scales, from overall plot structure to individual motifs, enabling both autonomous composition and co-creation with varying degrees of user control. Evaluation with compositions based on tales demonstrated the system's ability to compose music that supports narrative listening and aligns with its source narratives, while being perceived as familiar and enjoyable.

Abstract

Abstract
We address the layout optimization problem of deciding the number, the location, and the operational space of a set of Airborne Wind Energy (AWE) units, which overall constitute an AWE farm. The layout optimization problem in conventional wind farms, with standard wind turbines, is a well-studied subject; however, in the case of AWE, there are several new characteristics and challenges. While in the case of conventional wind farms, the main concern is to guarantee a reduced aerodynamical wake effect from other units, in AWE the main concern is to avoid collision among units. The optimization problem addressed is the following: given a specific land dimension and local wind characteristics, we solve a bi-objective problem of maximizing power production while minimizing the number of units, by deciding the number of producing units, their locations, as well as their flight envelopes. The solution method uses a combination of metaheuristic methods, including elements from the Non-Dominated Sorting Genetic Algorithm-II (NSGA-II) and the Biased Random Key Genetic Algorithm (BRKGA). The results produce a custom Pareto set adapted to the wind local characteristics, allowing for a more accurate estimation of the key objectives, better estimate of the annual power output of the AWE farm, and make better-informed decisions regarding the optimal number of units to deploy in the farm.