Abstract
This paper presents Alloy4Fun, a web application that enables online editing and sharing of Alloy models and instances (including dynamic ones developed with the Electrum extension), to be used mainly in an educational context. By introducing secret paragraphs and commands in the models, Alloy4Fun allows the distribution and automated assessment of simple specification challenges, a mechanism that enables students to learn the language at their own pace. Alloy4Fun stores all versions of shared and analyzed models, as well as derivation trees that depict how they evolved over time: this wealth of information can be mined by researchers or tutors to identify, for example, learning breakdowns in the class or typical mistakes made by Alloy users. A data analysis library is also provided to support this process. Alloy4Fun has been used in formal methods graduate courses for 3 years and for the latest editions we present results regarding its adoption by the students, as well as preliminary insights regarding the most common bottlenecks when learning Alloy (and Electrum).

Abstract
Many archival collections have been recently digitized and made available to a wide public. The contained documents however tend to have limited attractiveness for ordinary users, since content may appear obsolete and uninteresting. Archival document collections can become more attractive for users if suitable content can be recommended to them. The purpose of this research is to propose a new research direction of Archival Content Suggestion to discover interesting content from long-term document archives that preserve information on society history and heritage. To realize this objective, we propose two unsupervised approaches for automatically discovering interesting sentences from news article archives. Our methods detect interesting content by comparing the information written in the past with one created in the present to make use of a surprise effect. Experiments on New York Times corpus show that our approaches effectively retrieve interesting content. © 2021, Springer Nature Switzerland AG.

Abstract
Hash tries are a trie-based data structure with nearly ideal characteristics for the implementation of hash maps. Starting from a particular lock-free hash map data structure, named Lock-Free Hash Tries, we focus on solving the problem of memory reclamation without losing the lock-freedom property. To the best of our knowledge, outside garbage collected environments, there is no current implementation of hash maps that is able to reclaim memory in a lock-free manner. To achieve this goal, we propose an approach for memory reclamation specific to Lock-Free Hash Tries that explores the characteristics of its structure in order to achieve efficient memory reclamation with low and well-defined memory bounds. We present and discuss in detail the key algorithms required to easily reproduce our implementation by others. Experimental results show that our approach obtains better results when compared with other state-of-the-art memory reclamation methods and provides a competitive and scalable hash map implementation, if compared to lock-based implementations.

Abstract
Tampered multimedia content is being increasingly used in a broad range of cybercrime activities. The spread of fake news, misinformation, digital kidnapping, and ransomware-related crimes are amongst the most recurrent crimes in which manipulated digital photos and videos are the perpetrating and disseminating medium. Criminal investigation has been challenged in applying machine learning techniques to automatically distinguish between fake and genuine seized photos and videos. Despite the pertinent need for manual validation, easy-to-use platforms for digital forensics are essential to automate and facilitate the detection of tampered content and to help criminal investigators with their work. This paper presents a machine learning Support Vector Machines (SVM) based method to distinguish between genuine and fake multimedia files, namely digital photos and videos, which may indicate the presence of deepfake content. The method was implemented in Python and integrated as new modules in the widely used digital forensics application Autopsy. The implemented approach extracts a set of simple features resulting from the application of a Discrete Fourier Transform (DFT) to digital photos and video frames. The model was evaluated with a large dataset of classified multimedia files containing both legitimate and fake photos and frames extracted from videos. Regarding deepfake detection in videos, the Celeb-DFv1 dataset was used, featuring 590 original videos collected from YouTube, and covering different subjects. The results obtained with the 5-fold cross-validation outperformed those SVM-based methods documented in the literature, by achieving an average F1-score of 99.53%, 79.55%, and 89.10%, respectively for photos, videos, and a mixture of both types of content. A benchmark with state-of-the-art methods was also done, by comparing the proposed SVM method with deep learning approaches, namely Convolutional Neural Networks (CNN). Despite CNN having outperformed the proposed DFT-SVM compound method, the competitiveness of the results attained by DFT-SVM and the substantially reduced processing time make it appropriate to be implemented and embedded into Autopsy modules, by predicting the level of fakeness calculated for each analyzed multimedia file.

Abstract
Ca2+ imaging is a widely used microscopy technique to simultaneously study cellular activity in multiple cells. The desired information consists of cell-specific time series of pixel intensity values, in which the fluorescence intensity represents cellular activity. For static scenes, cellular signal extraction is straightforward, however multiple analysis challenges are present in recordings of contractile tissues, like those of the enteric nervous system (ENS). This layer of critical neurons, embedded within the muscle layers of the gut wall, shows optical overlap between neighboring neurons, intensity changes due to cell activity, and constant movement. These challenges reduce the applicability of classical segmentation techniques and traditional stack alignment and regions-of-interest (ROIs) selection workflows. Therefore, a signal extraction method capable of dealing with moving cells and is insensitive to large intensity changes in consecutive frames is needed. Here we propose a b-spline active contour method to delineate and track neuronal cell bodies based on local and global energy terms. We develop both a single as well as a double-contour approach. The latter takes advantage of the appearance of GCaMP expressing cells, and tracks the nucleus' boundaries together with the cytoplasmic contour, providing a stable delineation of neighboring, overlapping cells despite movement and intensity changes. The tracked contours can also serve as landmarks to relocate additional and manually-selected ROIs. This improves the total yield of efficacious cell tracking and allows signal extraction from other cell compartments like neuronal processes. Compared to manual delineation and other segmentation methods, the proposed method can track cells during large tissue deformations and high-intensity changes such as during neuronal firing events, while preserving the shape of the extracted Ca2+ signal. The analysis package represents a significant improvement to available Ca2+ imaging analysis workflows for ENS recordings and other systems where movement challenges traditional Ca2+ signal extraction workflows.

Abstract
The success achieved by using SAR data in the study of the Earth led to a firm commitment from space agencies to develop more and better space-borne SAR sensors. This involvement of the space agencies makes us believe that it is possible to increase the potential of SAR interferometry (InSAR) to near real-time monitoring. Among this ever-increasing number of sensors, the ESA's Sentinel-1 (C-band) mission stands out and appears to be disruptive. This mission is acquiring vast volumes of data making current analyzing approaches inviable. This amount of data can no longer be analyzed and studied using classic methods raising the need to use and create new techniques. We believe that Machine Learning techniques can be the solution to overcome this issue since they allow to train Deep Learning models to automate human processes for a vast volume of data. In this paper, we use deep learning models to automatically find and locate deformation areas in InSAR interferograms without atmospheric correction. We train three state-of-the-art classification models for detection deformation areas, achieving an AUC of 0.864 for the best model (VGG19 for wrapped interferograms). Additionally, we use the same models as encoders to train U-net models, achieving a Dice score of 0.54 for InceptionV3. It is necessary more data to achieve better results in segmentation.