Abstract
Context: Low-code development is a concept whose presence has grown both in academia and the software industry and is discussed alongside others, such as model-driven engineering and domain-specific languages. Usability is an important concept in low-code contexts since users of these tools often lack a background in programming. Grey literature articles have also stated that low-code tools have high usability.Objective: This paper examines the current literature about low-code and no-code to discover more about them and their relationship with usability, particularly its quality, which factors are the most relevant, and how users view these tools. This focus on usability aims to provide a different point of view from other works on low-code.Method: We performed a systematic literature review based on a formal protocol for this study. The search protocol returned a total of 207 peer-review articles across five databases, which was supplemented with a snowballing process. These were filtered using inclusion and exclusion criteria, resulting in 38 relevant articles that were analysed, synthesised and reported.Conclusion: Despite growing interest and a strong enterprise presence in academia, we did not find a formal definition of low-code, although common characteristics have been specified. We found that users have a heightened awareness of usability regarding low-code tools, with some authors performing feasibility studies on their implementations or listing factors that influence the user experience in a given tool. Researchers are considering usability factors unconsciously, and the low-code field would grow if research on usability increased. This paper also suggests a definition for low-code development.

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.