Abstract
The present study aimed to evaluate whether a 14-day period of balneotherapy influences the inflammatory status, health-related quality of life (QoL) and quality of sleep, underlying overall health state, and clinically relevant benefits of patients with musculoskeletal diseases (MD). The health-related QoL was evaluated using the following instruments: 5Q-5D-5L, EQ-VAS, EUROHIS-QOL, B-IPQ, and HAQ-DI. The quality of sleep was evaluated by a BaSIQS instrument. Circulating levels of IL-6 and C-reactive protein (CRP) were measured by ELISA and chemiluminescent microparticle immunoassay, respectively. The smartband, Xiaomi MI Band 4, was used for real-time sensing of physical activity and sleep quality. MD patients improved the health-related QoL measured by 5Q-5D-5L (p < 0.001), EQ-VAS (p < 0.001), EUROHIS-QOL (p = 0.017), B-IPQ (p < 0.001), and HAQ-DI (p = 0.019) after balneotherapy; the sleep quality was also improved (BaSIQS, p = 0.019). Serum concentrations of IL-6 were markedly decreased after the 14-day balneotherapy (p < 0.001). No statistically significant differences were observed regarding the physical activity and sleep quality data recorded by the smartband. Balneotherapy may be an effective alternative treatment in managing the health status of MD patients, with a decrease in inflammatory states, along with positive effects on pain reduction, patient's functionality, QoL, quality of sleep, and disability perception status.

Abstract
Byzantine Fault tolerant (BFT) protocols are implemented to guarantee the correct system/application behavior even in the presence of arbitrary faults (i.e., Byzantine faults). Byzantine Fault tolerant State Machine Replication (BFT-SMR) is a known software solution for masking arbitrary faults and malicious attacks (Liu et al., 2020). In this survey, we present and discuss relevant BFT-SMR protocols, focusing on deterministic and probabilistic approaches. The main purpose of this paper is to discuss the characteristics of proposed works for each approach, as well as identify the trade-offs for each different approach.& COPY; 2023 The Author(s). Published by Elsevier Ltd. This is an open access article under the CC BY license ( http://creativecommons.org/licenses/by/4.0/ )

Abstract
The Internet revolution in 1990, followed by the data-driven and information revolution, has transformed the world as we know it. Nowadays, what seam to be 10 to 20 years ago, a science fiction idea (i.e., machines dominating the world) is seen as possible. This revolution also brought a need for new regulatory practices where user trust and artificial Intelligence (AI) discourse has a central role. This work aims to clarify some misconceptions about user trust in AI discourse and fight the tendency to design vulnerable interactions that lead to further breaches of trust, both real and perceived. Findings illustrate the lack of clarity in understanding user trust and its effects on computer science, especially in measuring user trust characteristics. It argues for clarifying those notions to avoid possible trust gaps and misinterpretations in AI adoption and appropriation.

Abstract
The Benínar Dam, located in Southeastern Spain, is an earth-fill dam that has experienced filtration issues since its construction in 1985. Despite the installation of various monitoring systems, the data collected are sparse and inadequate for the dam’s lifetime. The present research integrates Multi-Temporal Interferometric Synthetic Aperture Radar (MT-InSAR) and dam modeling to validate the monitoring of this dam, opening the way to enhanced integrated monitoring systems. MT-InSAR was proved to be a reliable and continuous monitoring system for dam deformation, surpassing previously installed systems in terms of precision. MT-InSAR allowed the almost-continuous monitoring of this dam since 1992, combining ERS, Envisat, and Sentinel-1A/B data. Line-of-sight (LOS) velocities of settlement in the crest of the dam evolved from maximums of -6 mm/year (1992–2000), -4 mm/year (2002–2010), and -2 mm/year (2015–2021) with median values of -2.6 and -3.0 mm/year in the first periods (ERS and Envisat) and -1.3 mm/year in the Sentinel 1-A/B period. These results are consistent with the maximum admissible modeled deformation from construction, confirming that settlement was more intense in the dam’s early stages and decreased over time. MT-InSAR was also used to integrate the monitoring of the dam basin, including critical slopes, quarries, and infrastructures, such as roads, tracks, and spillways. This study allows us to conclude that MT-InSAR and dam modeling are important elements for the integrated monitoring systems of embankment dams. This conclusion supports the complete integration of MT-InSAR and 3D modeling into the monitoring systems of embankment dams, as they are a key complement to traditional geotechnical monitoring and can overcome the main limitations of topographical monitoring.

Abstract
We present an imperative refinement language for the development of backtracking programs and discuss its semantic foundations. For expressivity, our language includes prospective values and preference - the latter being a variant of Nelson's biased choice that backtracks from infeasibility of a continuation. Our key contribution is to examine feasibility-preserving refinement as a basis for developing backtracking programs, and several key refinement laws that enable compositional refinement in the presence of non -monotonic program combinators.

Abstract
Conflict-free Replicated Data Types (CRDTs) are a very popular class of distributed data structures that strike a compromise between strong and eventual consistency. Ensuring the protection of data stored within a CRDT, however, cannot be done trivially using standard encryption techniques, as secure CRDT protocols would require replica-side computation. This paper proposes an approach to lift general-purpose implementations of CRDTs to secure variants using secure multiparty computation (MPC). Each replica within the system is realized by a group of MPC parties that compute its functionality. Our results include: i) an extension of current formal models used for reasoning over the security of CRDT solutions to the MPC setting; ii) a MPC language and type system to enable the construction of secure versions of CRDTs and; iii) a proof of security that relates the security of CRDT constructions designed under said semantics to the underlying MPC library. We provide an open-source system implementation with an extensive evaluation, which compares different designs with their baseline throughput and latency.