Overview

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. 

Full Product Details

Author:   Maurice H. ter Beek ,  Leopoldo Teixeira
Publisher:   Springer Nature Switzerland AG
Imprint:   Springer Nature Switzerland AG
ISBN:  

9783032120854

ISBN 10:   3032120853
Pages:   243
Publication Date:   27 November 2025
Audience:   Professional and scholarly ,  College/higher education ,  Professional & Vocational ,  Postgraduate, Research & Scholarly
Format:   Paperback
Publisher's Status:   Active
Availability:   Not yet available  
This item is yet to be released. You can pre-order this item and we will dispatch it to you upon its release.

Table of Contents

.-  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.

Reviews

Author Information

Tab Content 6

Author Website:  

Countries Available

All regions