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.

Abstract

Abstract

Abstract
Immersive video applications impose unpractical bandwidth requirements for best-effort networks. With Multi-View(MV) streaming, these can be minimized by resorting to view prediction techniques. SmoothMV is a multi-view system that uses a non-intrusive head tracking mechanism to detect the viewer's interest and select appropriate views. By coupling Neural Networks (NNs) to anticipate the viewer's interest, a reduction of view-switching latency is likely to be obtained. The objective of this paper is twofold: 1) Present a solution for acquisition of gaze data from users when viewing MV content; 2) Describe a dataset, collected with a large-scale testbed, capable of being used to train NNs to predict the user's viewing interest. Tracking data from head movements was obtained from 45 participants using an Intel Realsense F200 camera, with 7 video playlists, each being viewed a minimum of 17 times. This dataset is publicly available to the research community and constitutes an important contribution to reducing the current scarcity of such data. Tools to obtain saliency/heat maps and generate complementary plots are also provided as an open-source software package.