ABSTRACT. This paper presents an abstract machine that can be easily used to teach intermediate and source code optimization, fundamental issues in a course on compiler construction techniques, bringing together theory and practice of computer science in a simple way.

ABSTRACT. In an industrial context, ad-hoc/manual testing strategies, using natural language, still seem to be highly prevalent since natural language descriptions are, more likely, easier to understand. Still, the lack of rigor can generate inaccurate tests. Aligned with other modern approaches, we promote the use of natural language descriptions with rigorously defined underlying semantics. As a distinguished feature of our approach, we cover the entire (direct engineering) testing process, from requirements to manual or automated test cases generated automatically. Requirements written in a controlled natural language are parsed, and their semantics are automatically modeled using the CSP process algebra. To address soundness and deal with different abstraction levels, we formalize the concept of a domain model, in which additional information, such as hierarchical composition and a dependence relation among test steps, is defined. Then, sound test cases are generated from the inferred scenarios using the \textit{cspio} conformance relation. These test cases, still expressed in CSP, can then be linearized back to natural language to allow manual execution or directly translated into test scripts for automated execution.

ABSTRACT. The presence of software is pervasive in the society, and, due to its impact on our routines, the concern about its quality and reliability is a matter of utmost importance, especially when it comes to critical systems. Although software testing is a crucial step in software production, it is typically associated with some risks and elevated costs, particularly, when carried out manually. Model-based testing (MBT) tools is a technique that is capable of changing this scenario, enabling automatic test design and execution. However, assessing the correctness of these tools, which are also software developed by humans, is a valid concern too. To alleviate this concern, formal testing approaches are proposed, encompassing a well-defined conformance relation, along with test generation and execution strategies. Moreover, it is typically expected a proof of the soundness of the proposed approach. Unfortunately, many of the devised conformance relations are only theoretically defined, or are associated with disconnected implementations, that is, with no rigorous guarantees that the proposed theory is implemented correctly. Here, we show how an industrial-strength interactive theorem prover (Rocq) can be used to simultaneously formalise and provide a correct mechanisation of conformance testing theories; bridging the gap between theory and practice.

ABSTRACT. The integration of machine learning (ML) into safety-critical railway systems raises significant challenges for certification, as current safety standards require transparent, fully specified system designs, whereas ML models are inherently opaque after training. This short paper presents an on-going work where a proof-of-concept architecture is explored, in which ML outputs are validated by an independently implemented safety controller. The controller is developed using the B method and deployed on a safety-grade computing platform, focusing on free-track detection as the application scenario. In this setup, a convolutional neural network proposes a candidate track path, and the safety controller verifies its consistency with physical and geometric constraints. The work illustrates how formal specification and proof can be applied to the safety component in order to constrain the influence of ML, without addressing the full certification process. This proof-of-concept highlights the potential for combining formally developed safety logic with advanced perception modules in railway applications, while acknowledging that further work is required for industrial deployment.