Abstract
One common characteristic among current lock-free memory allocators is that they rely on the operating system to manage memory since they lack a lower-level mechanism capable of splitting and coalescing blocks of memory. In this paper, we discuss this problem and we propose a generic scheme for an efficient lock-free best-fit coalescing-capable mechanism that is able of satisfying memory allocation requests with desirable low fragmentation characteristics.

Abstract
We report on the development of numerical module for the HiLight simulation platform based on GPGPU supercomputing to solve a system of coupled fields governed by the Generalized Nonlinear Schrodinger Equation with local and/or nonlocal nonlinearities. This models plays an important role in describing a plethora of different phenomena in various areas of physics. In optics, this model was initially used to describe the propagation of light through local and/or nonlocal systems under the paraxial approximation, but more recently it has been extensively used as a support model to develop optical analogues. However, establishing the relation between the original system and the analogue, as well as, between their model and the actual experimental setup is not an easy task. First and foremost because in most cases the governing equations are nonintegrable, preventing from obtaining analytical solutions and hindering the optimization of the experiments. Alternatively, despite numerical methods not providing exact solutions, they allow to test different experimental scenarios and provide a better insight to what to expect in an actual experiment, while giving access to all the variables of the optical system being simulated. However, the numerical solution of a system of N-coupled Schrodinger fields in systems with two or three spatial dimensions requires massive computation resources, and must employ advanced supercomputing and parallelization techniques, such as GPGPU. This paper focuses on the numerical aspects behind this challenge, describing the structure of our simulation module, its performance and the tests performed.

Abstract
The Sternum is a human bone located in the anterior area of the thoracic cage. It is present in most of the axial cuts provided from the Magnetic Resonance Imaging (MRI) acquisitions. used in the medical field. Detecting the Sternum is relevant as it contains rigid key-points for 3D model reconstructions, assisting in the planning and evaluation of several surgical procedures, and for atlas development by segmenting structures in anatomical proximity. In the absence of applicable approaches for this specific problem. this paper focuses on two distinct automated methods for Sternum segmentation in MRI. The first. relies on K-Means (Clustering) to perform the segmentation, while the second encompasses the closed Minimum Path over the elliptical transformation of Gradient images. A dataset of 14 annotated acquisitions was used for evaluation. The results favored the Gradient approach over Clustering.

Abstract
This paper presents a new, heterogeneous CPU+GPU attacks against lattice-based (post-quantum) cryptosystems based on the Shortest Vector Problem (SVP), a central problem in lattice-based cryptanalysis. To the best of our knowledge, this is the first SVP-attack against lattice-based cryptosystems using CPUs and GPUs simultaneously. We show that Voronoi-cell based CPU+GPU attacks, algorithmically improved in previous work, are suitable for the proposed massively parallel platforms. Results show that 1) heterogeneous platforms are useful in this scenario, as they increment the overall memory available in the system (as GPU's memory can be used effectively), a typical bottleneck for Voronoi-cell algorithms, and we have also been able to increase the performance of the algorithm on such a platform, by successfully using the GPU as a co-processor, 2) this attack can be successfully accelerated using conventional GPUs and 3) we can take advantage of multiple GPUs to attack lattice-based cryptosystems. Experimental results show a speedup up to 7.6x for 2 GPUs hosted by an Intel Xeon E5-2695 v2 CPU (12 cores x2 sockets) using only 1 core and gains in the order of 20% for 2 GPUs hosted by the same machine using all 22 CPU threads (2 are reserved for orchestrating the GPUs), compared to single-CPU execution using the entire 24 threads available.

Abstract
The paper is concerned with the practical use of formal techniques to contribute to the risk analysis of a new neonatal dialysis machine. The described formal analysis focuses on the controller component of the software implementation. The controller drives the dialysis cycle and deals with error management. The logic was analysed using model checking techniques and the source code was analysed formally, checking type correctness conditions, use of pointers and shared memory. The analysis provided evidence of the verification of risk control measures relating to the software component. The productive dialogue between the developers of the device, who had no experience or knowledge of formal methods, and the analyst using the formal analysis tools, provided a basis for the development of rationale for the effectiveness of the evidence.

Abstract
Recently, soft attention mechanisms have been successfully used in a wide variety of applications such as the generation of image captions, text translation, etc. This mechanism attempts to mimic the visual cortex of a human brain by not analyzing all the objects in a scene equally, but by looking for clues (or salient features) which might give a more compact representation of the environment. In doing so, the human brain can process information more quickly and without overloading. Having learned this lesson, in this paper, we try to make a bridge from the visual to the audio scene classification problem, namely the classification of heart sound signals. To do so, a novel approach merging soft attention mechanisms and recurrent neural nets is proposed. Using the proposed methodology, the algorithm can successfully learn automatically significant audio segments when detecting and classifying abnormal heart sound signals, both improving these classification results and somehow creating a simple justification for them.