SBMF 2025: 28TH BRAZILIAN SYMPOSIUM ON FORMAL METHODS

This page contains an index consisting of author-provided keywords.

A
Abstract machines	The Turner 2-Strings Machines
Action Model	Formal Verification of Epistemic States with Uncertainty in Multi-Agent Systems
Active Objects	Resource Contracts for Active Objects
applied formal methods	Industry panel
ASTD	A Modular Orthogonal Integration of Operational and Prescriptive Timing Requirements using TASTD
Automata Learning	Inference of Deterministic Finite Automata via Q-Learning
Availability modeling	Availability Model and Evaluation of Bus Rapid Transit Surveillance System
B
Banach-Tarski paradox	A Proof of the De Zolt Postulate in Three-dimensional Space
benchmarking	The Turner 2-Strings Machines
Bilattices	Formal Verification of Epistemic States with Uncertainty in Multi-Agent Systems
Bus Rapid Transit	Availability Model and Evaluation of Bus Rapid Transit Surveillance System
C
C Code Verification	Bridging the B-Method and ACSL: Towards Verified C Code
CCSL	A Modular Orthogonal Integration of Operational and Prescriptive Timing Requirements using TASTD
code performance	The Turner 2-Strings Machines
conformance testing	Executable Conformance Testing Theories: from Theory to Practice and Back
Contracts	Resource Contracts for Active Objects
Controlled Natural Language	Deriving Sound Test Scripts from Requirements written in a Controlled Natural Language
D
De Zolt's postulate	A Proof of the De Zolt Postulate in Three-dimensional Space
Domain Model	Deriving Sound Test Scripts from Requirements written in a Controlled Natural Language
Dynamic Epistemic Logic	Formal Verification of Epistemic States with Uncertainty in Multi-Agent Systems
E
Epistemic Logic	Formal Verification of Epistemic States with Uncertainty in Multi-Agent Systems
Execution Semantics	A Research Agenda for the Living SysML v2 Blueprint: Toward Executable, Verifiable, and Navigable System Models
F
formal method	A Modular Orthogonal Integration of Operational and Prescriptive Timing Requirements using TASTD
formal methods	Formal Development of a Safety Controller for Machine Learning Outputs in Vital Railway Systems State-based Security and Time-Inserting Supervisors Industry talk (TBA) Industry panel
Formal Semantics	Deriving Sound Test Scripts from Requirements written in a Controlled Natural Language
Formal Verification	A Research Agenda for the Living SysML v2 Blueprint: Toward Executable, Verifiable, and Navigable System Models Bridging the B-Method and ACSL: Towards Verified C Code
Formalization of Mathematics	A Proof of the De Zolt Postulate in Three-dimensional Space
H
hardware functional verification	Industry talk (TBA)
I
industrial applications	Industry talk (TBA)
industry	Industry panel
information flow	State-based Security and Time-Inserting Supervisors
Intermediate code optimization	The Turner 2-Strings Machines
ioco	Executable Conformance Testing Theories: from Theory to Practice and Back
IoT-based Monitoring Systems	Availability Model and Evaluation of Bus Rapid Transit Surveillance System
L
Lean	A Proof of the De Zolt Postulate in Three-dimensional Space
M
Maude	Resource Contracts for Active Objects
Model Checking	Formal Verification of Epistemic States with Uncertainty in Multi-Agent Systems
Multi-Valued Logic	Formal Verification of Epistemic States with Uncertainty in Multi-Agent Systems
O
opacity	State-based Security and Time-Inserting Supervisors
P
process algebra	State-based Security and Time-Inserting Supervisors
Q
Q-Learning	Inference of Deterministic Finite Automata via Q-Learning
R
railway	Formal Development of a Safety Controller for Machine Learning Outputs in Vital Railway Systems
reactive systems	Executable Conformance Testing Theories: from Theory to Practice and Back
Reinforcement Learning	Inference of Deterministic Finite Automata via Q-Learning
Reports on teaching formal methods	The Turner 2-Strings Machines
Resource Allocation	Resource Contracts for Active Objects
Rocq	Executable Conformance Testing Theories: from Theory to Practice and Back
RPNI	Inference of Deterministic Finite Automata via Q-Learning
S
safety critical	Formal Development of a Safety Controller for Machine Learning Outputs in Vital Railway Systems
security	State-based Security and Time-Inserting Supervisors
Smart cities	Availability Model and Evaluation of Bus Rapid Transit Surveillance System
Software Safety	Bridging the B-Method and ACSL: Towards Verified C Code
Source code optimization	The Turner 2-Strings Machines
SysML v2	A Research Agenda for the Living SysML v2 Blueprint: Toward Executable, Verifiable, and Navigable System Models
T
TASTD	A Modular Orthogonal Integration of Operational and Prescriptive Timing Requirements using TASTD
Test Case Consistency	Deriving Sound Test Scripts from Requirements written in a Controlled Natural Language
W
Workflow Models	Resource Contracts for Active Objects

Disclaimer | Powered by EasyChair Smart Program