This book constitutes the refereed proceedings of the 28th Brazilian Symposium on Formal Methods: Foundations and Applications, SBMF 2025, held in Recife, Brazil, during December 3–5, 2025.
The 12 full papers and 1 short paper included in this book were carefully reviewed and selected from 24 submissions. They were organized in topical sections as follows: Process Algebras and Time; Formal Verification; Testing; Availability and Contracts; Formal Methods and AI; and Teaching and Foundations.
Edited by:
Maurice H. ter Beek,
Leopoldo Teixeira
Imprint: Springer Nature Switzerland AG
Country of Publication: Switzerland
Dimensions:
Height: 235mm,
Width: 155mm,
ISBN: 9783032120854
ISBN 10: 3032120853
Series: Lecture Notes in Computer Science
Pages: 243
Publication Date: 27 November 2025
Audience:
Professional and scholarly
,
College/higher education
,
Undergraduate
,
Further / Higher Education
Format: Paperback
Publisher's Status: Active
.- Formal Reasoning for Assuring Product Lines of Complex Systems. .- Safe Evolution of Smart Contracts Supported by LLMs and Bounded Model Checking. .- Exploring Modelling Language Engineering. .- Process Algebras and Time .- State-based Security and Time-Inserting Supervisors. .- A Modular Orthogonal Integration of Operational and Prescriptive Timing Requirements using TASTD. .- Formal Verification .- Bridging the B-Method and ACSL: Towards Verified C Code. .- A Research Agenda for the Living SysML v2 Blueprint: Toward Executable, Verifiable, and Navigable System Models. .- Formal Verification of Epistemic States with Uncertainty in Multi-Agent Systems. .- Testing .- Deriving Sound Test Scripts from Requirements written in a Controlled Natural Language. .- Executable Conformance Testing Theories: from Theory to Practice and Back. .- Availability and Contracts .- Availability Model and Evaluation of Bus Rapid Transit Surveillance System. .- Resource Contracts for Active Objects. .- Formal Methods and AI .- Inference of Deterministic Finite Automata via Q-Learning. .- Formal Development of a Safety Controller for Machine Learning Outputs in Vital Railway Systems. .- Teaching and Foundations .- The Turner 2-Strings Machines. .- A Proof of the De Zolt Postulate in Three-dimensional Space.