Abstract
AbstractThe correction of artifacts in Magnetic Resonance Imaging (MRI) is crucial due to physiological phenomena and technical issues affecting diagnostic quality. Reverting from corrupted to artifact-free images is a complex task. Deep Learning (DL) models have been employed to preserve data characteristics and to identify and correct those artifacts. We proposeMAC, a novel DL-based solution to correct artifacts in multi-contrast brain MRI scans.MACoffers two models: the simulation and the correction models. The simulation model introduces perturbations similar to those occurring in an exam while preserving the original image as ground truth; this is required as publicly available datasets rarely have motion-corrupted images. It allows the addition of three types of artifacts with different degrees of severity. The DL-based correction model adds a fourth contrast to state-of-the-art solutions while improving the overall performance of the models.MACachieved the highest results in the FLAIR contrast, with a Structural Similarity Index Measure (SSIM) of 0.9803 and a Normalized Mutual Information (NMI) of 0.8030. Moreover, the model reduced training time by 63% compared to its predecessor.MACmodel can correct large volumes of images faster and adapt to different levels of artifact severity than current state-ofthe-art models, allowing for better diagnosis.

Abstract
AbstractWith the rapid growth of Deep Learning models and neural networks, the medical data available for training – which is already significantly less than other types of data – is becoming scarce. For that purpose, Generative Adversarial Networks (GANs) have received increased attention due to their ability to synthesize new realistic images. Our preliminary work shows promising results for brain MRI images; however, there is a need to distribute the workload, which can be supported by High-Performance Computing (HPC) environments. In this paper, we generate 256×256 MRI images of the brain in a distributed setting. We obtained an FIDRadImageNetof 10.67 for the DCGAN and 23.54 for the WGAN-GP, which are consistent with results reported in several works published in this scope. This allows us to conclude that distributing the GAN generation process is a viable option to overcome the computational constraints imposed by these models and, therefore, facilitate the generation of new data for training purposes.

Abstract
The availability of public services through online platforms has improved the coverage and efficiency of essential services provided to citizens worldwide. These services also promote transparency and foster citizen participation in government processes. However, the increased online presence also exposes sensitive data exchanged between citizens and service providers to a wider range of security threats. Therefore, ensuring the security and trustworthiness of online services is crucial to Electronic Government (EGOV) initiatives' success. Hence, this work assesses the security posture of online platforms hosted in 3068 governmental domain names, across all UN Member States, in three dimensions: support for secure communication protocols; the trustworthiness of their digital certificate chains; and services' exposure to known vulnerabilities. The results indicate that despite its rapid development, the public sector still falls short in adopting international standards and best security practices in services and infrastructure management. This reality poses significant risks to citizens and services across all regions and income levels.

Abstract
The design and analysis of systems that combine computational behaviour with physical processes' continuous dynamics - such as movement, velocity, and voltage - is a famous, challenging task. Several theoretical results from programming theory emerged in the last decades to tackle the issue; some of which are the basis of a proof-of-concept tool, called Lince, that aids in the analysis of such systems, by presenting simulations of their respective behaviours. However being a proof-of-concept, the tool is quite limited with respect to usability, and when attempting to apply it to a set of common, concrete problems, involving autonomous driving and others, it either simply cannot simulate them or fails to provide a satisfactory user-experience. The current work complements the aforementioned theoretical approaches with a more practical perspective, by improving Lince along several dimensions: to name a few, richer syntactic constructs, more operations, more informative plotting systems and errors messages, and a better performance overall. We illustrate our improvements via a variety of examples that involve both autonomous driving and electrical systems.

Abstract
Advancements in the energy efficiency and computational power of embedded devices allow developers to equip resource-constrained systems with a greater number of features and more complex behavior. As complexity of a system grows, so does the difficulty in demonstrating its overall correctness. Formal methods have been successfully applied in a variety of verification and validation scenarios, but their wide adoption in the industry and academia is still lackluster. Among the explanations listed in the literature for the low adoption of these techniques are the perceived difficulty of getting into formal practices and how formal tools are not usually aimed at practical use cases. Striving to address these issues, we present MARS, an open-source domain-specific language for the safe instrumentation of runtime verification monitors into real-time resource-constrained distributed systems. Our main objective with MARS is to ease the integration of runtime verification monitors in distributed applications while also providing developers with evidence of their correct instrumentation in the context of systems where dependability and temporal requirements need to be respected even under extreme resource constraints. We present the language syntax, the set of tools embedded into its compiler, its functionalities, and a use case to exemplify its use in a practical distributed application.

Abstract
A significant number of dependable systems rely on scheduling algorithms to achieve temporal correctness. Despite their relevance in real-world applications, only a narrow subset of the works in the literature of real-time systems are readily available to be reproduced in real-world hardware platforms. This lack of support not only hinders the reproducibility of research results, but also reduces the opportunity for new platform-specific research directions to emerge. In this work we discuss the use and development of an open-source tool named MARS capable of porting various scheduling tests and algorithms to hardware platforms used in distributed real-time dependable systems.