Abstract
Alloy is a lightweight formal specification language, supported by an IDE, which has proven well-suited for reasoning about software design in early development stages. The IDE provides a visualizer that produces graphical representations of analysis results, which is essential for the proper validation of the model. Alloy is a rich language but inherently static, so behavior needs to be explicitly encoded and reasoned about. Even though this is a common scenario, the visualizer presents limitations when dealing with such models. The main contribution of this paper is a principled approach to generate instance visualizations, which improves the current Alloy Visualizer, focusing on the representation of behavior.

Abstract
This paper reviews the first challenge on spectral image reconstruction from RGB images, i.e., the recovery of whole-scene hyperspectral (HS) information from a 3channel RGB image. The challenge was divided into 2 tracks: the "Clean" track sought HS recovery from noiseless RGB images obtained from a known response function (representing spectrally-calibrated camera) while the "Real World" track challenged participants to recover HS cubes from JPEG-compressed RGB images generated by an unknown response function. To facilitate the challenge, the BGU Hyperspectral Image Database [4] was extended to provide participants with 256 natural HS training images, and 5+ 10 additional images for validation and testing, respectively. The "Clean" and "Real World" tracks had 73 and 63 registered participants respectively, with 12 teams competing in the final testing phase. Proposed methods and their corresponding results are reported in this review.

Abstract
The introduction of Industry 4.0 to modernize the existing industrial manufacturing systems has created a wave of disruption all over the world, that changed not only the industry paradigm, but also the research directions in the intelligent manufacturing systems field. After five years since its presentation, similar initiatives have fostered in several countries worldwide to promote the adoption of Industry 4.0 principles. This paper aims to analyze and discuss the current state of adoption of this initiative and to verify the way it changed the research directions, particularly at the level of applying artificial intelligence and ICT technologies in the cyber-physical systems context. For this purpose, an analytical study of the scientific publications related to Industry 4.0 domain has been performed, considering a dataset of scientific publications retrieved from the IEEE Xplore database. This dataset considers two distinct time periods, separated by the introduction of Industry 4.0 as the digitalization threshold: before digital era (B.D.) and after digital era (A.D.). © 2018 IEEE.

Abstract
Objective: The main goal of this study was to develop an automatic method based on supervised learning methods, able to distinguish healthy from pathologic arterial pulse wave (APW), and those two from noisy waveforms (non-relevant segments of the signal), from the data acquired during a clinical examination with a novel optical system. Materials and methods: The APW dataset analysed was composed by signals acquired in a clinical environment from a total of 213 subjects, including healthy volunteers and non-healthy patients. The signals were parameterised by means of 39 pulse features: morphologic, time domain statistics, cross-correlation features, wavelet features. Multiclass Support Vector Machine Recursive Feature Elimination (SVM RFE) method was used to select the most relevant features. A comparative study was performed in order to evaluate the performance of the two classifiers: Support Vector Machine (SVM) and Artificial Neural Network (ANN). Results and discussion: SVM achieved a statistically significant better performance for this problem with an average accuracy of 0.9917 +/- 0.0024 and a F-Measure of 0.9925 +/- 0.0019, in comparison with ANN, which reached the values of 0.9847 +/- 0.0032 and 0.9852 +/- 0.0031 for Accuracy and F-Measure, respectively. A significant difference was observed between the performances obtained with SVM classifier using a different number of features from the original set available. Conclusion: The comparison between SVM and NN allowed reassert the higher performance of SVM. The results obtained in this study showed the potential of the proposed method to differentiate those three important signal outcomes (healthy, pathologic and noise) and to reduce bias associated with clinical diagnosis of cardiovascular disease using APW.

Abstract
A multimode interferometer based on an etched coreless optical fiber tip is proposed for the determination of the thermo-optic coefficient of ethanol-water mixtures, through refractive index and temperature measurements. © OSA 2018 © 2018 The Author(s)

Abstract
We study Authenticated Encryption with Associated Data (AEAD) from the viewpoint of composition in arbitrary (single-stage) environments. We use the indifferentiability framework to formalize the intuition that a "good" AEAD scheme should have random ciphertexts subject to decryptability. Within this framework, we can then apply the indifferentiability composition theorem to show that such schemes offer extra safeguards wherever the relevant security properties are not known, or cannot be predicted in advance, as in general-purpose crypto libraries and standards. We show, on the negative side, that generic composition (in many of its configurations) and well-known classical and recent schemes fail to achieve indifferentiability. On the positive side, we give a provably indifferentiable Feistel-based construction, which reduces the round complexity from at least 6, needed for blockciphers, to only 3 for encryption. This result is not too far off the theoretical optimum as we give a lower bound that rules out the indifferentiability of any construction with less than 2 rounds.