Abstract
Models-at different levels of abstraction and pertaining to different engineering views-are central in the design of railway networks, in particular signalling systems. The design of such systems must follow numerous strict rules, which may vary from project to project and require information from different views. This renders manual verification of railway networks costly and error-prone. This paper presents EVEREST, a tool for automating the verification of railway network models that preserves the loosely coupled nature of the design process. To achieve this goal, EVEREST first combines two different views of a railway network model-the topology provided in signalling diagrams containing the functional infrastructure, and the precise coordinates of the elements provided in technical drawings (CAD)-in a unified model stored in the railML standard format. This railML model is then verified against a set of user-defined infrastructure rules, written in a custom modal logic that simplifies the specification of spatial constraints in the network. The violated rules can be visualized both in the signalling diagrams and technical drawings, where the element(s) responsible for the violation are highlighted. EVEREST is integrated in a long-term effort of EFACEC to implement industry-strong tools to automate and formally verify the design of railway solutions. © 2022 ACM.

Abstract
We present a literature review that aims to understand the role of the Educational Escape Room (EER) in improving the teaching, learning, and assessment processes through an EER design framework. The main subject is to identify the recent interventions in this field in the last five years. Our study focuses on understanding how it is possible to create an EER available to all students, namely visually challenged users. As a result of the implementation of new learning strategies that promote autonomous learning, a concern arose in adapting educational activities to each student's individual needs. To study the adaptability of each EER, we found the EER design framework essential to increase the student experience by promoting the consolidation of knowledge through narrative and level design. The results of our study show evidence of progress in students' performance while playing an EER, revealing that students' learning can be effective. Research on Procedural Content Generation (PCG) highlighted how important it is to implement adaptability in future studies of EERs. However, we found some limitations regarding the process of evaluating learning through the EERs, showing how important it is to study and implement learning analytics in future studies in this field.

Abstract
This paper presents an educational resource to support the teaching of Portuguese sign language. This educational resource emerges in response to the significant needs for the development of adequate digital tools to support deaf people in different tasks, especially in the language learning process. This work is motivated by the results and conclusions from previous studies that identify augmented reality as one of the promising solutions to improve the learning and teaching processes, and benefits from the advances already accomplished in the development and application of augmented reality solutions in several domains of the educational environment. The educational resource presented in this work is an augmented reality solution that enables associating hand gestures, representative of Portuguese sign language, to different cards, which represent different letters of the alphabet. In this way, it is possible to associate the alphabet letters with the respective gestures in a visual and straightforward way, facilitating the learning process.

Abstract
Modelling complex information systems often entails the need for dealing with scenarios of inconsistency in which several requirements either reinforce or contradict each other. In this kind of scenarios, arising e.g. in knowledge representation, simulation of biological systems, or quantum computation, inconsistency has to be addressed in a precise and controlled way. This paper generalises Belnap-Dunn four-valued logic, introducing paraconsistent transition systems (PTS), endowed with positive and negative accessibility relations, and a metric space over the lattice of truth values, and their modal logic.

Abstract
When developing mobile applications, developers often have to decide when to acquire and when to release resources. This leads to resource leaks, a kind of bug where a resource is acquired but never released. This is a common problem in Android applications that can degrade energy efficiency and, in some cases, can cause resources to not function properly. In this paper, we present an extension of EcoAndroid, an Android Studio plugin that improves the energy efficiency of Android applications, with an inter-procedural static analysis that detects resource leaks. Our analysis is implemented using Soot, FlowDroid, and Heros, which provide a static-analysis environment capable of processing Android applications and performing inter-procedural analysis with the IFDS framework. It currently supports the detection of leaks related to four Android resources: Cursor, SQLite-Database, Wakelock, and Camera. We evaluated our tool with the DroidLeaks benchmark and compared it with 8 other resource leak detectors. We obtained a precision of 72.5% and a recall of 83.2%. Our tool was able to uncover 191 previously unidentified leaks in this benchmark. These results show that our analysis can help developers identify resource leaks.

Abstract