Abstract
This article addresses the optimal bidding strategy problem of a virtual power plant (VPP) participating in the day-ahead (DA), real-time (RT) and spinning reserve (SR) markets (SRMs). The VPP comprises a number of dispatchable energy resources (DERs), renewable energy resources (RESs), energy storage systems (ESSs) and a number of customers with flexible demand. A two-stage risk-constrained stochastic problem is formulated for the VPP scheduling, where the uncertainty lies in the energy and reserve prices, RESs production, load consumption, as well as calls for reserve services. Based on this model, the VPP bidding/offering strategy in the DA market (DAM), RT market (RTM) and SRM is decided aiming to maximize the VPP profit considering both supply and demand-sides (DS) capability for providing reserve services. On the other hand, customers participate in demand response (DR) programs by using load curtailment (LC) and load shifting (LS) options as well as by providing reserve service to minimize their consumption costs. The proposed model is implemented on a test VPP and the optimal decisions are investigated in detail through a numerical study. Numerical simulations demonstrate the effectiveness of the proposed scheduling strategy and its operational advantages and the computational effectiveness.

Abstract
Deductive verification has gained paramount attention from both academia and industry. Although intensive research in this direction covers almost all mainstream languages, the research community has paid little attention to the verification of database applications. This paper proposes a comprehensive set of Verification Conditions (VCs) generation techniques from database programs, adapting Symbolic Execution, Conditional Normal Form, and Weakest Precondition. The validity checking of the generated VCs for a database program determines its correctness w.r.t. the annotated database properties. The developed prototype DBverify based on our theoretical foundation allows us to instantiate VC generation from PL/SQL codes, yielding to detailed performance analysis of the three approaches under different circumstances. With respect to the literature, the proposed approach shows its competence to support crucial SQL features (aggregate functions, nested queries, NULL values, and set operations) and the embedding of SQL codes within a host imperative language. For the chosen set of benchmark PL/SQL codes annotated with relevant properties of interest, our experiment shows that only 38% of procedures are correct, while 62% violate either all or part of the annotated properties. The primary cause for the latter case is mostly due to the acceptance of runtime inputs in SQL statements without proper checking.

Abstract
Tourism has been a fundamental pillar for the development of the Portuguese economy and has supported and stimulated new opportunities. However, for small and medium enterprises (SMEs) in the hospitality sector, and given their specific characteristics, there are no specific indicators to monitor sustainability, and they are only based on existing generic models such as ETIS, WTO, and Green Globe. Given the complexity of the indicators in these models and their comprehensive vision, it makes it difficult for hospitality SMEs that have limited resources to measure them. Consequently, it is important to focus their attention on the most relevant indicators for their activity. In this sense, this study is relevant in identifying the critical sustainability factors for Portuguese hospitality SMEs. In total, and after the synthesis and assessment of the various indicators, a total of 35 critical indicators were identified, distributed among the economic, social, sustainable management, and environmental dimensions.

Abstract
The last years saw the emergence of nonlinear optical materials, with local and nonlocal nonlinearities, as experimentally accessible systems to implement optical analogues of quantum fluids. In these systems, a light beam propagating in the nonlinear medium can be interpreted as a fluid, where the diffraction in the transverse plane to the propagation gives the effective mass of the fluid and the medium nonlinearity mediates the required interactions between the photons. This fluid interpretation and its application have been extensively studied, from the creation of superfluid-like flows and the study of phenomena associated with this effect to the implementation of gravity analogues. Furthermore, many optical materials have been considered, with a special interest in the ones that offer tunable mechanisms that allow to easily control the system properties to better explore and emulate the different phenomena. Recently, nematic liquid crystals have been proposed as an interesting tunable material capable of supporting superfluids of light. These systems have a nonlocal character and offer external mechanisms that can be used to tailor the nonlinearity to better emulate the desired analogue system. Indeed, through the application of an external electric field perpendicular to the direction of propagation, is it possible to control the nonlocal length of the nonlinearity. This mechanism offers interesting opportunities in the present context. In this work, through numerical methods based on GPGPU supercomputing, we explore the possibility of observing superfluid effects in defocusing nematic liquid crystals. In particular, we explore the possibility of observing the drag force cancellation and the emission of quantized vortices, which are two manifestations of a superfluid flow. Furthermore, we also discuss the possibility of using these systems for creating an analogue of quantum turbulence with these materials. These studies constitute a stepping-stone towards the implementation of gravity analogues with nematic liquid crystals.

Abstract
Adaptive Deep Brain Stimulation has recently emerged to tackle conventional DBS limitations by measuring disease fluctuations and to adapt stimulation parameter accordingly. In early 2020, Medtronic launched in the European Union the first certified DBS neurostimulator capable of simultaneously stimulate and read signals from the deep brain structures, the PerceptTMPC. In epilepsy, the most common target brain structure is the Anterior Nucleus of Thalamus and the Local Field Potentials analysis requires prior synchronization of data recorded from the Percept PC with video-Electroencephalography (vEEG) equipment. Fine-grained synchronization (sub-second resolution) is mandatory for multimodal neurodata analysis and may be achieved by aligning artefacts perceived in both systems. In this work we study two methods aiming for neurodata streams clock synchronization: one based on DBS stimulation artefacts and another on tapping maneuver artefacts. For this purpose, we studied the data collected from the first epileptic patient that underwent 1-week vEEG-PerceptTMPC monitoring at a Hospital monitoring unit. We found that tapping maneuver-based methodology allowed a more accurate synchronization in relation to the stimulation artefact-based method (0.56s vs. 2.07s absolute average uncertainty). This method was also more complete one since tapping timestamps can be determined by video timeframes and do not require a prior identification of artefacts in EEG data by clinicians.

Abstract
Modern communications have moved away from point-to-point models to increasingly heterogeneous network models. In this article, we propose a novel controller-based architecture to deploy adaptive causal network coding in heterogeneous and highly meshed communication networks. Specifically, we consider using the software-defined network as the main controller. We first present an architecture for highly meshed heterogeneous multi-source multi-destination networks that represent the practical communication networks encountered in the fifth generation of wireless networks and beyond. Next, we present a promising solution to deploy network coding over the new architecture. We also present a new controller-based setting with which network coding modules communicate to attain the required information. Finally, we briefly discuss how the proposed architecture and network coding solution provide a good opportunity for future technologies.