Proceedings of the Brazilian Symposium on Formal Methods (SBMF)

Current Issue

2025: Proceedings of the 28th Brazilian Symposium on Formal Methods

The Proceedings of the 28th Brazilian Symposium on Formal Methods (SBMF 2025) bring the papers selected and presented in the edition of the event held in Recife/PE, Brazil, from December 03-05, 2025. In this issue, the proceedings include 12 full papers and 01 short paper. These papers were selected through a single-blind review, from a total of 24 full papers and 01 short paper submitted, which implied an acceptance rate of 50% and 100%, respectively. The event's program committee was coordinated by Leopoldo Teixeira (UFPE, Brazil) and Maurice ter Beek (ISTI-CNR, Italy), who organized this volume. The articles in this volume were submitted on 08/15/2025, accepted for publication on 09/26/2025, with the final version submitted on 10/13/2025.

You can find more information about SBMF 2025 by visiting the website of the event.

Published: 2025-12-03

Opening

Front Matter

Leopoldo Teixeira, Maurice ter Beek

i-xviii
- Springer

Full Papers

State-Based Security and Time-Inserting Supervisors

Damas P. Gruska

3-18
- Springer
A Modular Orthogonal Integration of Operational and Prescriptive Timing Requirements Using TASTD

Alex Rodrigue Ndouna, Marc Frappier, Frédéric Mallet

19-36
- Springer
Bridging the B-Method and ACSL: Towards Verified C Code

Fagner M. Dias, Marcel V. M. Oliveira, Thierry Lecomte

39-60
- Springer
A Research Agenda for the Living SysML V2 Blueprint: Toward Executable, Verifiable, and Navigable System Models

Ciprian Teodorov, Lucas Lima, Sidney C. Nogueira, Sylvain Guerin, Loïc Lagadec

61-81
- Springer
Formal Verification of Epistemic States with Uncertainty in Multi-Agent Systems

Jefferson O. Andrade

82-97
- Springer
Deriving Sound Test Scripts from Requirements Written in a Controlled Natural Language

Filipe Arruda, Flávia Barros, Augusto Sampaio

101-118
- Springer
Executable Conformance Testing Theories: From Theory to Practice and Back

Gustavo Carvalho, Lucas Santana, Fábio Sobral, Beatriz Souza

119-137
- Springer
Availability Model and Evaluation of Bus Rapid Transit Surveillance System

Raquel F. Trajano, Carlos Melo, Jamilson Dantas

141-155
- Springer
Resource Contracts for Active Objects

Charaf Eddine Dridi, Violet Ka I Pun, Volker Stolz

156-175
- Springer
Traditional approaches to inference of deterministic finite-state automata (DFA) 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). This paper investigates the use of Q-learning, a well-known reinforcement learning algorithm, for the passive inference of deterministic finite automata. It builds on the core insight 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. The paper demonstrates how Q-learning can be adapted for automaton inference and provides an evaluation on several examples.

Elaheh Hosseinkhani, Martin Leucker

179-195
- Springer
The Turner 2-Strings Machines

Rafael Dueire Lins

209-224
- Springer
A Proof of the De Zolt Postulate in Three-Dimensional Space

Bruno Cuconato, Edward Hermann Haeusler

225-241
- Springer

Short Papers

Formal Development of a Safety Controller for Machine Learning Outputs in Vital Railway Systems

Thierry Lecomte

196-206
- Springer

View All Issues