Abstract
The offset tracking technique based on synthetic aperture radar (SAR) image intensity information can estimate glacier displacement even when glacier velocities are high and the time interval between images is long, allowing for the broad use of this technique in glacier velocity monitoring. Terrestrial laser scanners, a non-contact measuring system, can measure the velocity of a glacier even if there are no control points arranged on a glacier. In this study, six COSMO-SkyMed images acquired between 31 July and 22 December 2016 were used to obtain the glacial movements of five glaciers on the northern slope of the central Himalayas using the offset tracking approach. During the period of image acquirement, a terrestrial laser scanner was used, and point clouds of two periods in a small area at the terminus of the Pingcuoliesa Glacier were obtained. By selecting three fixed areas of the point clouds that have similar shapes across two periods, the displacements of the centers of gravity of the selected areas were calculated by using contrast analyses of feature points. Although the overall low-density point clouds data indicate that the glacial surfaces have low albedos relative to the wavelength of the terrestrial laser scanner and the effect of its application is therefore influenced in this research, the registration accuracy of 0.0023 m/d in the non-glacial areas of the scanner's measurements is acceptable, considering the magnitude of 0.072 m/d of the minimum glacial velocity measured by the scanner. The displacements from the point clouds broadly agree with the results of the offset tracking technique in the same area, which provides further evidence of the reliability of the measurements of the SAR data in addition to the analyses of the root mean squared error of the velocity residuals in non-glacial areas. The analysis of the movement of five glaciers in the study area revealed the dynamic behavior of these glacial surfaces across five periods. G089972E28213N Glacier, Pingcuoliesa Glacier and Shimo Glacier show increasing surface movement velocities from the terminus end to the upper part with elevations of 1500 m, 4500 m, and 6400 m, respectively. The maximum velocities on the glacial surface profiles were 31.69 cm/d, 62.40 cm/d, and 42.00 cm/d, respectively. In contrast, the maximum velocity of Shie Glacier, 50.60 cm/d, was observed at the glacier's terminus. For each period, G090138E28210N Glacier exhibited similar velocity values across the surface profile, with a maximum velocity of 39.70 cm/d. The maximum velocities of G089972E28213N Glacier, Pingcuoliesa Glacier, and Shie Glacier occur in the areas where the topography is steepest. In general, glacial surface velocities are higher in the summer than in the winter in this region. With the assistance of a terrestrial laser scanner with optimized wavelengths or other proper ground-based remote sensing instruments, the offset tracking technique based on high-resolution satellite SAR data should provide more reliable and detailed information for local and even single glacial surface displacement monitoring.

Abstract
Today's climatic proneness to extreme conditions together with human activity have been triggering a series of wildfire-related events that put at risk ecosystems, as well as animal and vegetal patrimony, while threatening dwellers nearby rural or urban areas. When intervention teams-firefighters, civil protection, police-acknowledge these events, usually they have already escalated to proportions hardly controllable mainly due wind gusts, fuel-like solo conditions, among other conditions that propitiate fire spreading. Currently, there is a wide range of camera-capable sensing systems that can be complemented with useful location data-for example, unmanned aerial systems (UAS) integrated cameras and IMU/GPS sensors, stationary surveillance systems-and processing components capable of fostering wildfire events detection and monitoring, thus providing accurate and faithful data for decision support. Precisely in what concerns to detection and monitoring, Deep Learning (DL) has been successfully applied to perform tasks involving classification and/or segmentation of objects of interest in several fields, such as Agriculture, Forestry and other similar areas. Usually, for an effective DL application, more specifically, based on imagery, datasets must rely on heavy and burdensome logistics to gather a representative problem formulation. What if putting together a dataset could be supported in customizable virtual environments, representing faithful situations to train machines, as it already occurs for human training in what regards some particular tasks (rescue operations, surgeries, industry assembling, etc.)? This work intends to propose not only a system to produce faithful virtual environments to complement and/or even supplant the need for dataset gathering logistics while eventually dealing with hypothetical proposals considering climate change events, but also to create tools for synthesizing wildfire environments for DL application. It will therefore enable to extend existing fire datasets with new data generated by human interaction and supervision, viable for training a computational entity. To that end, a study is presented to assess at which extent data virtually generated data can contribute to an effective DL system aiming to identify and segment fire, bearing in mind future developments of active monitoring systems to timely detect fire events and hopefully provide decision support systems to operational teams. © 2019 International Society for Photogrammetry and Remote Sensing.

Abstract
COSMO-SkyMed is a constellation of four X-band high-resolution radar satellites with a minimum revisit period of 12 hours. These satellites can obtain ascending and descending synthetic aperture radar (SAR) images with very similar periods for use in the three-dimensional (3D) inversion of glacier velocities. In this paper, based on ascending and descending COSMO-SkyMed data acquired at nearly the same time, the surface velocity of the Yiga Glacier, located in the Jiali County, Tibet, China, is estimated in four directions using an offset tracking technique during the periods of 16 January to 3 February 2017 and 1 February to 19 February 2017. Through the geometrical relationships between the measurements and the SAR images, the least square method is used to retrieve the 3D components of the glacier surface velocity in the eastward, northward and upward directions. The results show that applying the offset tracking technique to COSMO-SkyMed images can be used to derive the true 3D velocity of a glacier's surface. During the two periods, the Yiga Glacier had a stable velocity, and the maximum surface velocity, 2.4 m/d, was observed in the middle portion of the glacier, which corresponds to the location of the steepest slope.

Abstract
Health consumers usually face difficulties on their online searches, mainly because of the differences between terminologies used by laypeople and health professionals. This work presents a tool, HealthTranslator, available as a Google Chrome extension that intends to reduce this terminological gap while users are searching the Web for health information. HealthTranslator automatically annotates medical concepts in web documents, providing additional information, such as concept definition, related concepts and links to external references. The solution was evaluated regarding its: ( a) performance-the document processing is done gradually, typically from the top to the bottom of the document and performance was not an issue raised by the users; ( b) concept coverage-the solution was compared to a similar extension performing in English recognizing significantly more concepts. A comparison with a corpus of Portuguese documents manually annotated with medical concepts showed an average F-measure between 27% and 33%, depending on the type of concepts being recognized; ( c) users' receptivity to HealthTranslator and its usability-many aspects were surveyed on a user study. In general, the extension has a good acceptance and users find it useful.

Abstract
Formal modeling and automatic analysis are essential to achieve a trustworthy software design prior to its implementation. Alloy and its Analyzer are a popular language and tool for this task. Frequently, rather than a single software artifact, the goal is to develop a full software product line (SPL) with many variants supporting different features. Ideally, software design languages and tools should provide support for analyzing all such variants (e.g., by helping pinpoint combinations of features that could break a property), but that is not currently the case. Even when developing a single artifact, support for multi-variant analysis is desirable to explore design alternatives. Several techniques have been proposed to simplify the implementation of SPLs. One such technique is to use background colors to identify the fragments of code associated with each feature. In this paper we propose to use that same technique for formal design, showing how to add support for features and background colors to Alloy and its Analyzer, thus easing the analysis of software design variants. Some illustrative examples and evaluation results are presented, showing the benefits and efficiency of the implemented technique. © Springer Nature Switzerland AG 2019.

Abstract
Most model checkers provide a useful simulation mode, that allows users to explore the set of possible behaviours by interactively picking at each state which event to execute next. Traditionally this simulation mode cannot take into consideration additional temporal logic constraints, such as arbitrary fairness restrictions, substantially reducing its usability for debugging the modelled system behaviour. Similarly, when a specification is false, even if all its counter-examples combined also form a set of behaviours, most model checkers only present one of them to the user, providing little or no mechanism to explore alternatives. In this paper, we present a simple on-the-fly verification technique to allow the user to explore the behaviours that satisfy an arbitrary temporal logic specification, with an interactive process akin to simulation. This technique enables a unified interface for simulating the modelled system and exploring its counter-examples. The technique is formalised in the framework of state/event linear temporal logic and a proof of concept was implemented in an event-based variant of the Electrum framework. © J. Brunel, D. Chemouil, A. Cunha, & N. Macedo.