Abstract
This document presents the case study for the ABZ 2023 conference. The case study introduces a safety critical interactive system called AMAN (Arrival MANager), which is a partly-autonomous scheduler of landing sequences of aircraft in airports. This interactive systems interleaves Air Traffic Controllers activities with automation in AMAN. While some AMAN systems are currently deployed in airports, we consider here only a subset of functions which represent a challenge in modelling and verification.

Abstract
In the current technological scenario of artificial intelligence growth, especially using machine learning, large datasets are necessary. Recommender systems appear with increasing frequency with different techniques for information filtering. Few large wine datasets are available for use with wine recommender systems. This work presents X-Wines, a new and consistent wine dataset containing 100,000 instances and 21 million real evaluations carried out by users. Data were collected on the open Web in 2022 and pre-processed for wider free use. They refer to the scale 1-5 ratings carried out over a period of 10 years (2012-2021) for wines produced in 62 different countries. A demonstration of some applications using X-Wines in the scope of recommender systems with deep learning algorithms is also presented.

Abstract
The study of the evacuation of buildings in emergency fire situations has deserved the attention of researchers for decades, particularly regarding the real-time guiding of occupants in their way to exit the building. However, finding solutions to guide the occupants evacuating a building requires a thorough knowledge of that domain. Using ontological models to model the knowledge of a domain allows the understanding of that domain to be shared. This paper presents an ontological model that pretends to reinforce and deepen knowledge of the domain under study and help develop solutions and systems capable of guiding the occupants during a building evacuation. The ontology was developed following the METHONTOLOGY methodology, and for implementation, the Protege tool was used. The ontological model was successfully submitted to a thorough evaluation process and is publicly available on the Web.

Abstract
Designing systems to serve a large number of people, who have similar demands, but also have varied needs and generate a huge volume of data, requires a software architecture that allows constant evolution, is easy to maintain, and has the ability to scale smartly. The SPL technique with microservices architecture seems promising to meet these requirements, but this integration is not trivial. Thus, we conduct a SLR that identified 3 architectures that proposed the combination of these techniques. However, the architectures found were complex and reduced time-to-market, as they proposed the implementation of all resources through microservices. Thus, in order to reduce the complexity of development and, consequently, reduce the time to market, this work presents a proposal for the design of a hybrid SPL architecture, through the combination of large backend APIs and microservices. In addition, this research paper presents a case study that consisted of defining the architecture of a medical clinics SPL as a Multi-tenant Software as a Service. Finally, we compare the complexity of the architecture generated using our approach, with a microservice architecture constructed using other approach found in literature.

Abstract
With the incresasing importance of program verification, an issue that has been receiving more attention is the certification of verification tools, addressing the vernacular question: Who verifies the verifier?. In this paper we approach this meta-verification problem by focusing on a fundamental component of program verifiers: the Verification Conditions Generator (VCGen), responsible for producing a set of proof obligations from a program and a specification. The semantic foundations of VCGens lie in program logics, such as Hoare logic, Dynamic logic, or Separation logic, and related predicate transformers. Dynamic logic is the basis of the KeY system, one of the foremost deductive verifiers, whose logic makes use of the notion of update, which is quite intricate to formalize. In this paper we derive systematically, based on a KeY-style dynamic logic, a correct-by-construction VCGen for a toy programming language. Our workflow covers the entire process, from the logic to the VCGen. It is implemented in the Why3 tool, which is itself a program verifier. We prove the soundness and (an appropriate notion of) completeness of the logic, then define a VCGen for our language and establish its soundness. Dynamic logic is one of a variety of research topics that our dear friend and colleague Luis Soares Barbosa has, over the years, initiated and promoted at the University of Minho. It is a pleasure for us to dedicate this work to him on the occasion of his 60th birthday.

Abstract
Gamma radiation over the Atlantic Ocean was measured continuously from January to May 2020 by a NaI(Tl) detector installed on board the Portuguese navy's ship NRP Sagres. Enhancements in the gamma radiation values are identified automatically by an algorithm for detection of anomalies in mean and variance as well as by visual inspection. The anomalies are typically +50% above the background level and relatively rare events (similar to<10% of the days). All the detected anomalies are associated with simultaneous precipitation events, consistent with the wet deposition of scavenged radionuclides. The enhancements are detected in the open ocean even at large distances (+500 km) from the nearest coastline. Back trajectories reveal that half of these events are associated with air masses experiencing continental land influences, but the other half do not display evidence of recent land contact. The enhancements in gamma radiation very far from land and with no evidence of continental fetch from back trajectories are difficult to explain as resulting only from radionuclides with a terrestrial source such as radon and its progeny. Further investigation and additional measurements are needed to improve understanding on the sources of ambient radioactivity in the open ocean and assess whether gamma radiation in the marine environment is influenced not only by radionuclides of terrestrial origin, but also cosmogenic radionuclides, like Beryllium-7, formed in the upper atmosphere but with the ability to be transported downward and serve as a tracer of the aerosols to which it attaches. Plain Language Summary Radioactive elements such as the noble gas radon and those produced by its radioactive decay are naturally present in the environment and used as tracers of atmospheric transport and composition. In particular, the noble gas radon, being inert and of predominantly terrestrial origin, is used to identify pristine marine air masses with no land contamination. Precipitation over land typically brings radon from the atmosphere to the surface, enhancing gamma radiation on the ground, but such enhancements have not been identified before nor expected over the ocean due to the low amount of radon typical of marine air masses. Here we report, for the first time, gamma radiation enhancements associated with precipitation in the oceanic environment, using measurements performed over the Atlantic Ocean in a campaign onboard the Portuguese navy ship NRP Sagres.