Abstract
EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify post-quantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.

Abstract
This paper presents a self-scheduling model for home energy management systems (HEMS) in which a novel formulation of a linear discomfort index (DI) is proposed, incorporating the preferences of end-users in the daily operation of home appliances. The HEMS self-scheduling problem is modelled as a mixed-integer linear programming (MILP) multi-objective problem, aimed at minimizing the energy bill and DI. In this framework, the proposed DI determines the optimal time slots for the operation of home appliances while minimizing end-users? bills. The resulting multi-objective optimization problem has then been solved by using the epsilon-constraint technique and the VIKOR decision maker has been employed to select the most desired Pareto solution. The proposed model is tested considering tariffs in the presence of various price-based demand response programs (DRP), namely time-of-use (TOU) and real-time pricing (RTP). In addition, different scenarios considering the presence of electrical energy storage (EES) are investigated to study their impact on the optimal operation of HEMS. The simulation results show that the self-scheduling approach proposed in this paper yields significant reductions in the electricity bills for different electricity tariffs.

Abstract
Background: Biogenic amines (BAs) are compounds considered to be contaminants of foodstuff and are cause of poisoning. The main BAs found in foods are cadaverine, putrescine, tyramine, histamine, spermine and spermidine. The number of food poisoning cases associated with BAs in food has increased in the recent years reinforcing the need for early detection to ensure high levels of food quality and safety. Scope and approach: This review aims to provide a general approach to the different BAs detected in foods their concentrations and sample treatments. These compounds are found in varying concentrations in a wide variety of foods such as fish, meat, fruits, vegetables, cheese, wine, and beer. It also refers the different analytical techniques currently used for the detection of BAs, as well as the different treatments of the samples and innovations of the techniques currently used that allow greater sensitivity and speed of the analyzes and with obtaining detection limits lower and lower. Key findings and conclusions: BAs are present in a wide variety of foods and their concentration is highly influenced by the storage conditions of food products. BAs can be precursors of nitrosamines, which have been linked to carcinogenic and mutagenic activity. Several analytical techniques and sample treatments have been improved in the last few years for better and faster detection of BAs.

Abstract
Organizations have been challenged by the need to process an increasing amount of data, both structured and unstructured, retrieved from heterogeneous sources. Criminal investigation police are among these organizations, as they have to manually process a vast number of criminal reports, news articles related to crimes, occurrence and evidence reports, and other unstructured documents. Automatic extraction and representation of data and knowledge in such documents is an essential task to reduce the manual analysis burden and to automate the discovering of names and entities relationships that may exist in a case. This paper presents SEMCrime, a framework used to extract and classify named-entities and relations in Portuguese criminal reports and documents, and represent the data retrieved into a graph database. A 5WH1 (Who, What, Why, Where, When, and How) information extraction method was applied, and a graph database representation was used to store and visualize the relations extracted from the documents. Promising results were obtained with a prototype developed to evaluate the framework, namely a name-entity recognition with an F-Measure of 0.73, and a 5W1H information extraction performance with an F-Measure of 0.65.

Abstract

Abstract
Introduction Type 2 diabetes mellitus (T2DM) is a major cause of blindness, kidney failure, myocardial infarction, stroke and lower limb amputation. We are still unable, however, to accurately predict or identify which patients are at a higher risk of deterioration. Most risk stratification tools do not account for novel factors such as sociodemographic determinants, self-management ability or access to healthcare. Additionally, most tools are based in clinical trials, with limited external generalisability. Objective The aim of this work is to design and validate a machine learning-based tool to identify patients with T2DM at high risk of clinical deterioration, based on a comprehensive set of patient-level characteristics retrieved from a population health linked dataset. Sample and design Retrospective cohort study of patients with diagnosis of T2DM on 1 January 2015, with a 5-year follow-up. Anonymised electronic healthcare records from the Whole System Integrated Care (WSIC) database will be used. Preliminary outcomes Outcome variables of clinical deterioration will include retinopathy, chronic renal disease, myocardial infarction, stroke, peripheral arterial disease or death. Predictor variables will include sociodemographic and geographic data, patients' ability to self-manage disease, clinical and metabolic parameters and healthcare service usage. Prognostic models will be defined using multidependence Bayesian networks. The derivation cohort, comprising 80% of the patients, will be used to define the prognostic models. Model parameters will be internally validated by comparing the area under the receiver operating characteristic curve in the derivation cohort with those calculated from a leave-one-out and a 10 times twofold cross-validation. Ethics and dissemination The study has received approvals from the Information Governance Committee at the WSIC. Results will be made available to people with T2DM, their caregivers, the funders, diabetes care societies and other researchers.