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. Traditional approaches to DFA inference stem from symbolic AI, including both active learning methods (e.g., Angluin’s L* algorithm and its variants) and passive techniques (e.g., Biermann and Feldman’s method, RPNI). Meanwhile, sub-symbolic AI, particularly machine learning, offers alternative paradigms for learning from data, such as supervised, unsupervised, and reinforcement learning (RL). In this paper, we investigate the use of Q-learning, a well-known reinforcement learning algorithm, for the passive inference of deterministic finite automata. Our core insight is that the learned Q-function, which maps state-action pairs to rewards, can be reinterpreted as the transition function of a DFA over a finite domain. This provides a novel bridge between sub-symbolic learning and symbolic representations. We demonstrate how Q-learning can be adapted for automaton inference and provide an evaluation on several examples.

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.