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 Protégé 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.

Abstract
The expansion of augmented reality across society, its availability in mobile platforms and the novelty character it embodies by appearing in a growing number of areas, have raised new questions related to people's predisposition to use this technology in their daily life. Acceptance models, which have been updated following technological breakthroughs and society changes, are known to be great tools for predicting the intention to use a new technological system. This paper proposes a new acceptance model aiming to ascertain the intention to use augmented reality technology in heritage sites-the Augmented Reality Acceptance Model (ARAM). ARAM relies on the use of the Unified Theory of Acceptance and Use of Technology model (UTAUT) model's constructs, namely performance expectancy, effort expectancy, social influence, and facilitating conditions, to which the new and adapted constructs of trust expectancy, technological innovation, computer anxiety and hedonic motivation are added. This model was validated with data gathered from 528 participants. Results confirm ARAM as a reliable tool to determine the acceptance of augmented reality technology for usage in cultural heritage sites. The direct impact of performance expectancy, facilitating conditions and hedonic motivation is validated as having a positive influence on behavioural intention. Trust expectancy and technological innovation are demonstrated to have a positive influence on performance expectancy whereas hedonic motivation is negatively influenced by effort expectancy and by computer anxiety. The research, thus, supports ARAM as a suitable model to ascertain the behavioural intention to use augmented reality in new areas of activity.

Abstract
Learning to program requires diligent practice and creates room for discovery, trial and error, debugging, and concept mapping. Learners must walk this long road themselves, supported by appropriate and timely feedback. Providing such feedback in programming exercises is not a humanly feasible task. Therefore, the early and steadily growing interest of computer science educators in the automated assessment of programming exercises is not surprising. The automated assessment of programming assignments has been an active area of research for over a century, and interest in it continues to grow as it adapts to new developments in computer science and the resulting changes in educational requirements. It is therefore of paramount importance to understand the work that has been performed, who has performed it, its evolution over time, the relationships between publications, its hot topics, and open problems, among others. This paper presents a bibliometric study of the field, with a particular focus on the issue of automatic feedback generation, using literature data from the Web of Science Core Collection. It includes a descriptive analysis using various bibliometric measures and data visualizations on authors, affiliations, citations, and topics. In addition, we performed a complementary analysis focusing only on the subset of publications on the specific topic of automatic feedback generation. The results are highlighted and discussed.