Abstract
In this paper we enhance the EasyCrypt proof assistant to reason about 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 previously lacking. 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 we present a new formalization of Universal Composability (UC).

Abstract
To stimulate research in the area of automotive electronics and electric vehicles, the IEEE Vehicular Technology Society (VTS) initiated the Motor Vehicles Challenge. The objective of the 2021 edition of this challenge is to provide a benchmark problem for the energy management of a dual-motor electric vehicle. To solve this, we propose a pragmatic optimization-based energy management system (EMS) that minimizes the instantaneous power consumption of the vehicle through manipulation of torque distribution ratios among the electric motors. Numerical results obtained with the VTS benchmark simulation model demonstrate that the proposed EMS can extend the vehicle range up to 3% when compared to baseline solutions.

Abstract
The main objective of the present research is to identify the knowledge flows responsible for promoting the innovation capacity of Portuguese companies. Specifically, we intend to identify which variables influence Portuguese innovation capacity from a macro and micro perspective, so that we can establish possible ways to promote open innovation (OI) in Portugal since Portuguese companies have little maturity in terms of open innovation when compared to companies in other countries of the European Union. To achieve this goal, the methodological design used consisted of two phases. In the first phase, a literature review was conducted to identify the main variables associated with innovation performance. After identifying the most influential variables in the literature, in a second phase, data were collected through three distinct databases, namely Pordata, the Portuguese Tax and Customs Authority, and SABI. To identify the most influential variables in the Portuguese innovation capacity, the multivariate multiple regression technique based on the ordinary least square (OLS) method was applied. The results of the present research bring empirical evidence that researchers dedicated to R&D from non-profit institutions (i.e., inbound OI) and researchers from firms (i.e., outbound OI) exert a significant influence on innovation capacity so the development of an optimal strategy for the strengthening of open innovation by Portuguese firms should take into account the use and combination of these two specific knowledge flows. In this sense, the originality of this research lies in the fact that it is the first attempt to understand the possible implications of the determinants of innovation capacity on open innovation, from an exploratory study concerning the flows of knowledge.

Abstract
Over the last decades clinical research has been driven by informatics changes nourished by distinct research endeavors. Inherent to this evolution, several issues have been the focus of a variety of studies: multi-location patient data access, interoperability between terminological and classification systems and clinical practice and records harmonization. Having these problems in mind, the Data Safe Haven paradigm emerged to promote a newborn architecture, better reasoning and safe and easy access to distinct Clinical Data Repositories. This study aim is to present a novel solution for clinical search harmonization within a safe environment, making use of a hybrid coding taxonomy that enables researchers to collect information from multiple repositories based on a clinical domain query definition. Results show that is possible to query multiple repositories using a single query definition based on clinical domains and the capabilities of the Unified Medical Language System, although it leads to deterioration of the framework response times. Participants of a Focus Group and a System Usability Scale questionnaire rated the framework with a median value of 72.5, indicating the hybrid coding taxonomy could be enriched with additional metadata to further improve the refinement of the results and enable the possibility of using this system as data quality tagging mechanism.

Abstract
Wikipedia is a free, multilingual, and collaborative online encyclopedia. Nowadays, it is one of the largest sources of online knowledge, often appearing at the top of the results of the major search engines, being one of the most sought-after resources by the public searching for health information. The collaborative nature of Wikipedia raises security concerns since this information is used for decision-making, especially in the health area. Despite being available in hundreds of idioms, there are asymmetries between idioms, namely regarding their quality. In this work, we compare the quality of health information on Wikipedia between idioms with 100 million native speakers or more, and also in Greek, Italian, Korean, Turkish, Persian, Catalan and Hebrew, for historical tradition. Quality metrics are applied to health and medical articles in English, maintained by WikiProject Medicine, and their versions in the above idioms. With this, we contribute to a clarification of the role of Wikipedia in the access to health information. We demonstrate differences in both the quantity and quality of information available between idioms. English is the idiom with the highest quality in general. Urdu, Greek, Indonesian, and Hindi achieved lower values of quality.

Abstract
We study price personalization in a two period duopoly with vertically differentiated products. In the second period, a firm not only knows the purchase history of all customers, as in standard Behavior Based Price Discrimination models, but it also collects detailed information on its old customers, using it to engage in price personalization. The analysis reveals that there exists a natural market for each firm, defined as the set of customers that cannot be poached by the rival in the second period. The equilibrium is unique, except when firms are ex-ante almost identical. In equilibrium, only the firm with the largest natural market poaches customers from the rival. This firm has highest profits but not necessarily the largest market share. Aggregate profits are lower than under uniform pricing. All consumers gain, total welfare is higher herein than under uniform pricing if firms' natural markets are sufficiently asymmetric. The low quality firm chooses the minimal quality level and a quality differential arises, though the exact choice for the high quality depends upon the cost specification.