Abstract
In this work, we enhance the EasyCrypt proof assistant to reason about the computational complexity of adversaries. The key technical tool is a Hoare logic for reasoning about computational complexity (execution time and oracle calls) of adversarial computations. Our Hoare logic is built on top of the module system used by EasyCrypt for modeling adversaries. We prove that our logic is sound w.r.t. the semantics of EasyCrypt programs-we also provide full semantics for the EasyCrypt module system, which was lacking previously. We showcase (for the first time in EasyCrypt and in other computer-aided cryptographic tools) how our approach can express precise relationships between the probability of adversarial success and their execution time. In particular, we can quantify existentially over adversaries in a complexity class and express general composition statements in simulation-based frameworks. Moreover, such statements can be composed to derive standard concrete security bounds for cryptographic constructions whose security is proved in a modular way. As a main benefit of our approach, we revisit security proofs of some well-known cryptographic constructions and present a new formalization of universal composability.

Abstract
Sectorization is the division of a large area, territory or network into smaller parts considering one or more objectives. Dynamic sectorization deals with situations where it is convenient to discretize the time horizon in a certain number of periods. The decisions will not be isolated, and they will consider the past. The application areas are diverse and increasing due to uncertain times. This work proposes a conceptualization of dynamic sectorization and applies it to a distribution problem with variable demand. Furthermore, Genetic Algorithm is used to obtain solutions for the problem since it has several criteria; Analytical Hierarchy Process is used for the weighting procedure. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract
Distribution networks are vulnerable to natural hazards which can cause major social and economic consequences. Identifying vulnerable areas and developing operational strategies, such as dispatching mobile energy systems, can help mitigate the effects of extreme events. Conventional approaches, mainly N-1/N-2 contingency security analysis, are efficient but they do not fully provide a comprehensive picture of the stochastic nature of the hazard impact. Stochastic approaches are more accurate but in general they are computationally expensive and hence not practical for the resilient operational decision-making of distribution system operators. Therefore, this paper develops a novel framework based on an adjacency-resource matrix (ARM) and an unsupervised machine learning algorithm to first identify vulnerable nodes. Next, these vulnerable nodes are utilized in the mitigation stage in order to minimize the expected energy not served (EENS) against a natural hazard. The efficiency of the proposed framework is tested on a 125-node Portuguese distribution system.

Abstract
The IVY workbench is a model-based tool for the formal modelling and verification of interactive systems. The tool uses model checking to carry out the verification step. The goal is not to replace, but to complement more exploratory and iterative user-centred design approaches. However, the need for formal and rigorous modelling and reasoning raises challenges for the integration of both approaches. This paper presents a new plugin that aims to provide support for the integration of the formal methods based analysis supported by the tool, with user-centred design. The plugin is described, and an initial validation of its functionalities presented.

Abstract
Team resilience is a critically essential contributor to team effectiveness. However, the impact of team resilience on project management success has been little studied. This article aims to investigate the influence of team resilience on project management success in the context of information system projects. Using a quantitative study, we show that there is a significant positive relationship between project team resilience and project management success. As a result of this finding, we stress the importance of developing actions to promote team resilience to increase the likelihood of project management success, particularly in unstable environments.

Abstract
E-commerce is a field that changed how consumers purchase and interact with products. Although, inherent limitations such as the difficulty of testing the products first-hand before a purchase can compromise consumers' trust in online purchases. Virtual Reality (VR) has been investigated as a tool to solve limitations in several fields and how we can harness its potential to improve the overall user experience. This study analysed how immersive VR (IVR) could solve these limitations by allowing consumers to test products beforehand. We have studied how the Novelty Factor (evaluated by the users' past VR experience) and Immersive Tendencies correlate with the users' Purchase Intention and Memory (how well they remember the product's characteristics). We have analysed a sample of 38 participants (21 males) from 18 to 28 years old. Participants experienced a refrigerator with an interactive touchscreen in an IVR setup and were guided through its functionalities. Results indicated that memory of the product's characteristics was positively correlated with how recently they experienced VR. No correlations were found in the female sample. A negative correlation between Purchase Intention and Memory of the product's characteristics was found in the male sample. We concluded that IVR applications could become helpful for both consumers and online shops in an e-commerce context regardless of the Novelty Factor and Immersive Tendencies of consumers. However, differences between genders should be further investigated.