Abstract
In recent years, code-reuse attacks have been used to exploit software vulnerabilities and gain control of numerous software programs and embedded devices. Several measures have been put in place to prevent this type of attack, such as Control-Flow Integrity (CFI) systems, and some of these systems have already been integrated into hardware. Nevertheless, Function-Oriented Programming (FOP) attacks, a form of code-reuse that chains functions to carry out malicious actions, continue to persist. In this work, we present the first analysis of the implications and feasibility of FOP attacks on microcontrollers, focusing on ARM Cortex-M processors that support PACBTI, that is, a hardware feature designed for CFI system implementation. During this process, we identified multiple dispatch gadgets in two common Real-time Operating System (RTOS). Since these gadgets reside within core OS functionalities, they are inherently included in a broad range of embedded operating systems. Furthermore, we also present CortexMFopper - a tool specially built to identify FOP gadgets in embedded devices and to raise awareness of this technique.

Abstract
Distributed Hash Tables (DHTs) remain to this day a central component of modern peer-to-peer (P2P) systems, which rely on complex DHT protocols to scale to millions of nodes. The correct operation of DHTs is therefore essential for the proper functioning of these systems. For this reason, formal methods have been employed to model and verify a range of correctness properties of various DHT protocols. However, these verification efforts have focused on protocol-specific properties, such as topological invariants, instead of functional properties. This focus limits our understanding of the precise guarantees offered by each protocol. We propose a protocol-independent axiomatization of DHT properties using Allen Temporal Logic (ATL). To validate our axiomatization, we have implemented it in the Alloy analyser and used our implementation both to establish a number of DHT-derived properties and to generate a set of DHT execution traces that cover an exhaustive list of DHT corner case behaviours.

Abstract
This paper presents an overview of the FGPE (Framework for Gamified Programming Education), a set of three Erasmus+ projects aimed at providing a framework for applying gamification to programming education. The overview will encompass all three phases of the framework development, emphasizing the gamification elements embedded in the design and implementation of the outputs of each phase. These outputs will be presented as a unified narrative, including the gamification framework for programming exercises, a format for defining gamification details for programming exercises and courses, the authoring tool for the gamification layer, a gamification Web service, a tutorial on gamifying programming exercises (guidance material), and a tool that automatically generates gamified programming exercises.

Abstract
In this paper we present results on the normalized temperature sensitivity of UV- and fs-induced fiber Bragg gratings in a singlemode fiber with similar to 4.7 mol% GeO2 and having an Ormocer coating. In the 1500-1600 nm wavelength range, the former shows an almost constant value of 6.165x10(-6) K-1, whilst the fs-induced present some variation not related with the strength of the grating but probably due to induced birefringence. The average value obtained was 6.191x10(-6) K-1 which is higher than the former. For the UV-induced gratings in the Corning SMF-28 fiber (3.67 mol% GeO2) the value obtained was 6.143x10(-6) K-1. The achieved values are compatible with the use of Corning 7980 silica-based cladding fiber. Preliminary results also show no measurable impact of the hydrogenation process or the strength of the grating on the normalized temperature sensitivity.

Abstract
The recent updates of the National Energy and Climate Plans (NECPs) for Portugal and Spain have some significant changes compared to the previous 2019 versions, especially for the Portuguese side where a greater demand and renewable generation capacity are foreseen. This work assesses the impact of these new plans on the Iberian electricity market (MIBEL) main outcomes using CEVESA market model. Simulation results allow the analysis of the expected generation mix and prices, CO2 emissions, system cost, system adequacy, interconnections capacity usage, H2 demand impact and its contribution to provide balancing flexibility, under different simulation scenarios.

Abstract
TLA(+) is one of the most popular formal methods for designing concurrent and distributed systems. TLA(+) specifications can be verified with the TLC model checker, but unfortunately only one user-specified configuration of the system is verified at a time. If configurations are simple (e.g. the number of processes in a concurrent algorithm) it is viable to run TLC for several configurations to gain confidence that the system indeed works correctly for all of them. However, for complex configurations it is difficult to do so, and critical configurations can easily be missed. This paper introduces Blast, a tool that simplifies this task, by enabling the user to easily verify a TLA(+) specification for all configurations inside a given scope. Our evaluation using a large benchmark of TLA(+) examples, shows that Blast can be effectively used in a wide range of specifications and helped us uncover issues in several of them.