SBMF 2025 is the twenty-eighth of a series of events devoted to the development, dissemination, and use of formal methods for the construction of high-quality computational systems. It is now a well-established event with an international reputation. It regularly receives submissions and participants from all over the world.
                    The main topics discussed at SBMF include: 
                    Formal aspects of specification languages and theoretical foundations, such as the development of
                    new
                    domain-specific languages, the formalization of existing languages, and the study of the foundations
                    of
                    software engineering.
                    Formal aspects of systems development, such as the application of formal methods to the development
                    of
                    cyber-physical systems, embedded systems, and software-intensive systems.
                    Verification and validation, such as the formal verification of the correctness of software systems,
                    the
                    model checking of the requirements of software systems, and the fuzz testing of software systems.
                    Formal verification of neural networks, such as the application of formal methods to the
                    verification of
                    the correctness of deep learning models.
                    Self-formalization and formal aspects in practice, such as the automation of formal methods, the use
                    of
                    formal methods in industrial settings, and the teaching of formal methods.
                
Previous SBMF proceedings on https://link.springer.com/conference/sbmf
The detailed program is available at: https://easychair.org/smart-program/SBMF2025/
| TIME | Tuesday (02/12)  | 
                                Wednesday (03/12)  | 
                                Thursday (04/12)  | 
                                Friday (05/12)  | 
                            
|---|---|---|---|---|
| 08:00 | REGISTRATION | REGISTRATION | REGISTRATION | REGISTRATION | 
| 08:30 | ETMF Opening Session | SBMF Opening Session | ||
| 09:00 | Lecture 1 | Keynote: Augusto Sampaio | Keynote: Hans Vangheluwe | Keynote: Marsha Chechik | 
| 09:30 | ||||
| 10:00 | ||||
| 10:30 | COFFEE BREAK | COFFEE BREAK | COFFEE BREAK | COFFEE BREAK | 
| 11:00 | Lecture 1 | Technical Session #1 | 
                                Technical Session #3 | 
                                Technical Session #4 | 
                            
| 11:30 | ||||
| 12:00 | ||||
| 12:30 | LUNCH BREAK | LUNCH BREAK | LUNCH BREAK | SBMF Closing Session | 
| 13:00 | - | |||
| 13:30 | - | |||
| 14:00 | Lecture 2 | Discussion Panel | Industrial Session | - | 
| 14:30 | - | |||
| 15:00 | - | |||
| 15:30 | COFFEE BREAK | COFFEE BREAK | COFFEE BREAK | - | 
| 16:00 | Lecture 2 | Technical Session #2 | 
                                CEMF Meeting | - | 
| 16:30 | - | |||
| 17:00 | - | |||
| 17:30 | - | - | - | |
| 18:00 | - | - | - | - | 
| 18:30 | - | - | - | - | 
| 19:00 | - | - | - | - | 
| 19:30 | - | - | CONFERENCE DINNER | - | 
| 20:00 | - | - | - | |
| 20:30 | - | - | - | |
| 21:00 | - | - | - | |
| 21:30 | - | - | - | |
| 22:00 | - | - | - | 
SBMF aims to provide a venue for the presentation and discussion of high-quality work in formal methods. The topics include, but are not limited to, the following:
                            Hans Vangheluwe is a Professor in the Antwerp Systems and Software Modelling (AnSyMo) group within the Computer Science Department at the University of Antwerp in Belgium, where he is a founding member of the NEXOR Consortium on Cyber-Physical Systems (CPS). AnSyMo is a Core Research Lab of Flanders Make, the strategic research centre for the Flemish manufacturing industry. He heads the Modelling, Simulation and Design Lab (MSDL), founded when he was a professor at McGill University in Montreal, Canada. In a variety of projects, often with industrial partners, he develops and applies the model-based theory and techniques of Multi-Paradigm Modelling (MPM) in application domains as diverse as bio-actived sludge waste-water treatment plant design and optimization (which led to the WEST commercial tool), safe automotive software (within the NECSIS project), and autonomic production plants in the context of Industry 4.0. His fundamental work covers the foundations of modelling and (co-)simulation, of model management, model transformation, and collaborative domain-specific (visual) modelling environments. In the mid ’90s, he was one of the original members of the equation-based, object-oriented modelling language Modelica design team, one of the initiatives of the ESPRIT Basic Research Working Group 8467 on “simulation for the future: new concepts, tools and applications” (SiE) which he co-founded. He has published extensively in simulation and in software modelling, including the relationship between modelling and formal methods. He is known for his motto “model everything explicitly …”.
                            Marsha Chechik is Professor and former Chair in the Department of Computer Science at the University of Toronto, where she holds Bell University Labs Chair in Software Engineering. In 2022, she served as Acting Dean in Faculty of Information. Her research interests are in the application of formal methods to improve the quality of software. She has co-authored numerous papers in formal methods, software specification and verification, computer safety and security, and requirements engineering. She is a member of IFIP Working Group 2.9 on Requirements Engineering, an Associate Editor-in-Chief of IEEE Transactions on Software Engineering and Associate Editor-in-Chief of Journal on Software and Systems Modeling. She has been Program Committee Chair of top software engineering and verification conferences: ASE’14, ESEC/FSE’21, TACAS’16, ICSE’18, FM’23, MODELS’24. She is Fellow of ACM, Fellow of Automated Software Engineering and Chair of ACM SIGSOFT.
                            Augusto Sampaio is a Full Professor of Software Engineering at the Federal University of Pernambuco (UFPE) in Brazil, where he has been a faculty member since 1995. He received his Ph.D. from the University of Oxford and later held postdoctoral positions at both Oxford and the University of York. His research focuses on formal methods in software engineering, with contributions to the semantics, refinement, and transformation of concurrent and object-oriented models and programs; compositional model checking; model-based testing; and the integration of formal and semi-formal approaches. He has coordinated major national and international projects, including the European FP7 COMPASS project, and long-term collaborations with Motorola and Embraer. He played a leading role in the creation of Brazil’s pioneering “Software Residency” model for industry-oriented training in software testing, awarded by the Brazilian Ministry of Science and Technology. Augusto is a recipient of numerous honors, including the Brazilian National Order of Scientific Merit (Commander), the Doctor Honoris Causa from the University of York, and the SBC Award for Scientific Merit. He is a member of the Pernambuco Science Academy, as well as the Brazilian Science Academy, and has been Chair of the Formal Methods Europe Fellowship Award Committee. He has served on the program committees of leading international conferences in formal methods and is Program Co-Chair of FM 2026, the 27th International Symposium on Formal Methods.
| Abstract submission | |
| Paper submission deadline | |
| September 26th, 2025 | Acceptance notice | 
| Camera-ready copy deadline | |
| December 2nd, 2025 | ETMF 2025 | 
| December 3rd to 5th, 2025 | SBMF 2025 | 
However, it is recommended to carefully read the information below to know the conditions and deadlines related to the registration. All registration fees are in Brazilian reais (R$/BRL).
Choose from the table below how do you plan to participate and then click here to register!
* Full discount at ETMF exclusively for undergraduate students.
** Conference Dinner included.
| Event | Category | SBMF | SBMF + SBC membership | ETMF | ETMF + SBC membership | 
|---|---|---|---|---|---|
| 19/Sep - 12/Oct | Undergraduate Student – SBC Member | R$ 50,00 | R$ 83,00 | R$ 0,00* | R$ 33,00 | 
| Undergraduate Student – non SBC Member | R$ 88,00 | R$ 83,00 | R$ 0,00* | R$ 33,00 | |
| Graduate Student – SBC Member | R$ 110,00 | R$ 245,00 | R$ 50,00 | R$ 185,00 | |
| Graduate Student – non SBC Member | R$ 256,00 | R$ 245,00 | R$ 190,00 | R$ 185,00 | |
| Basic Education Teacher – SBC Member | R$ 165,00 | R$ 300,00 | R$ 50,00 | R$ 185,00 | |
| Basic Education Teacher – non SBC Member | R$ 317,00 | R$ 300,00 | R$ 190,00 | R$ 185,00 | |
| Federal Education Teacher – SBC Member | R$ 175,00 | R$ 545,00 | R$ 50,00 | R$ 420,00 | |
| Federal Education Teacher – non SBC Member | R$ 563,00 | R$ 545,00 | R$ 425,00 | R$ 420,00 | |
| Professional – SBC Member | R$ 200,00** | R$ 575,00** | R$ 50,00** | R$ 425,00** | |
| Professional – non SBC Member | R$ 595,00** | R$ 575,00** | R$ 430,00** | R$ 425,00** | |
| 13/Oct - 09/Nov | Undergraduate Student – SBC Member | R$ 60,00 | R$ 93,00 | R$ 0,00* | R$ 33,00 | 
| Undergraduate Student – non SBC Member | R$ 99,00 | R$ 93,00 | R$ 0,00* | R$ 33,00 | |
| Graduate Student – SBC Member | R$ 140,00 | R$ 275,00 | R$ 70,00 | R$ 205,00 | |
| Graduate Student – non SBC Member | R$ 289,00 | R$ 275,00 | R$ 212,00 | R$ 205,00 | |
| Basic Education Teacher – SBC Member | R$ 190,00 | R$ 325,00 | R$ 70,00 | R$ 205,00 | |
| Basic Education Teacher – non SBC Member | R$ 344,00 | R$ 325,00 | R$ 212,00 | R$ 205,00 | |
| Federal Education Teacher – SBC Member | R$ 200,00 | R$ 570,00 | R$ 70,00 | R$ 440,00 | |
| Federal Education Teacher – non SBC Member | R$ 590,00 | R$ 570,00 | R$ 447,00 | R$ 440,00 | |
| Professional – SBC Member | R$ 220,00** | R$ 595,00** | R$ 70,00** | R$ 445,00** | |
| Professional – non SBC Member | R$ 617,00** | R$ 595,00** | R$ 452,00** | R$ 445,00** | |
| 09/Nov - 05/Dec | Undergraduate Student – SBC Member | R$ 70,00 | R$ 103,00 | R$ 0,00* | R$ 33,00 | 
| Undergraduate Student – non SBC Member | R$ 110,00 | R$ 103,00 | R$ 0,00* | R$ 33,00 | |
| Graduate Student – SBC Member | R$ 160,00 | R$ 295,00 | R$ 90,00 | R$ 225,00 | |
| Graduate Student – non SBC Member | R$ 311,00 | R$ 295,00 | R$ 234,00 | R$ 225,00 | |
| Basic Education Teacher – SBC Member | R$ 200,00 | R$ 335,00 | R$ 90,00 | R$ 225,00 | |
| Basic Education Teacher – non SBC Member | R$ 355,00 | R$ 335,00 | R$ 234,00 | R$ 225,00 | |
| Federal Education Teacher – SBC Member | R$ 210,00 | R$ 580,00 | R$ 90,00 | R$ 460,00 | |
| Federal Education Teacher – non SBC Member | R$ 601,00 | R$ 580,00 | R$ 469,00 | R$ 460,00 | |
| Professional – SBC Member | R$ 240,00** | R$ 615,00** | R$ 90,00** | R$ 465,00** | |
| Professional – non SBC Member | R$ 639,00** | R$ 615,00** | R$ 474,00** | R$ 465,00** | 
Non-SBC members or members with an annual fee that is about to expire can join or renew their membership along with their registration, choosing the COMBO categories with a discount on the registration fee.
The COMBO categories are the most advantageous option for non-SBC members, as the registration fees are lower than the categories without combo and include SBC membership.
Visit the SBC website and see why you should become a member.
Becoming a member of SBC is a way to make SBC even stronger to represent our area of work with the various sectors. How about becoming part of our Community?
Some exclusive member benefits:
Payment of enrollments can be made by means of bank slip, credit card, debit in Banco do Brasil account, purchase order or invoice.
Enrollments can be made until the last day of the event, however payments by debit and bill will be accepted until November 28th, 2025.
Enrollments by purchase order or invoice:
The participant must access the enrollment system and register, selecting the payment method "purchase order" or "invoice" and clicking on pay. The system will provide the information necessary for the enrollment to be confirmed.
Registration for SBMF authors. Papers accepted to SBMF will be published in a volume of LNCS. At least one author (professional or student) of each accepted paper must be registered for SBMF 2025. Authors can not use the registration benefits (exemption or 50% discount) granted by SBC to affiliated institutions. The author registration must be paid until October 13th, 2025.
Until November 16th, 2025, a refund of 50% of the registration fee for SBMF/ETMF may be requested. After this date, no refunds will be issued. This policy applies both to the cancellation of the registration itself and to the cancellation of any additional activities. To request a cancellation, please send your request to faturamento@sbc.org.br .
                        Lucas Lima
(Universidade Federal Rural de Pernambuco, Brazil)
                        Leopoldo Teixeira
(Informatics Center, Federal University of Pernambuco, Brazil)
                        Maurice ter Beek
(ISTI-CNR, Pisa)
                        Diego Ferreira
(Universidade Federal Rural de Pernambuco, Brazil)
                        Vince Molnár
(Budapest University of Technology and Economics, Hungary)
                        Lucas Lima
(Universidade Federal Rural de Pernambuco, Brazil)
                        Yoni Zohar
(Bar-Ilan University, Israel)
                        Haniel Barbosa
(Universidade Federal de Minas Gerais, Brazil)
                        Ciprian Teodorov
(ENSTA-Bretagne, France)
                        Sidney C. Nogueira
(Universidade Federal Rural de Pernambuco, Brazil)
We invite submissions of papers with a strong emphasis on formal methods, whether practical or theoretical, in the following categories:
The page limits exclude references and appendices.
Contributions should not be simultaneously submitted for publication elsewhere. They should be written in English, and prepared using Springer’s Lecture Notes in Computer Science (LNCS) format. Springer’s proceedings LaTeX templates are available in Overleaf. More information is available at the following link: https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines
Papers should present unpublished and original work that has a clear contribution to the state-of-the-art on the theory and practice of formal methods. Papers will be judged by at least three reviewers based on originality, relevance, technical soundness, and presentation quality and should contain sound theoretical or practical results. Industry papers should emphasize the practical application of formal methods or report on open challenges.
Submissions should be made via this link: https://easychair.org/conferences/?conf=sbmf2025
We plan that accepted papers will be published, after the conference, in a volume of LNCS. The authors will be requested to complete and sign a consent-to-publish form. Every accepted paper MUST have at least one author registered in the symposium by the time the camera-ready copy is submitted. The registered author is also expected to attend the symposium and present the paper.
To be confirmed: We plan to follow on last years' tradition of organizing a special issue of the Science of Computer Programming Journal (Elsevier) with selected and extended papers from the 28th Brazilian Symposium on Formal Methods (SBMF 2025).
 
            Recife, a vibrant coastal city in northeastern Brazil, is the capital of the state of Pernambuco and one of the most important cultural, economic, and technological hubs in the region. Known as the "Brazilian Venice" due to its many rivers, bridges, and historical architecture, Recife is a city rich in history, art, and innovation.
            
            Located at the meeting point of the Beberibe and Capibaribe rivers before they flow into the Atlantic Ocean, Recife boasts a unique landscape that blends colonial heritage with modern urban development. The city's historic center, Recife Antigo, is home to landmarks such as the Paço do Frevo, dedicated to the traditional Frevo dance and music, and the Marco Zero, the symbolic starting point of Recife.
            
            One of the city's most famous attractions is the Instituto Ricardo Brennand, a cultural complex with an extensive collection of European and Brazilian art, and the Oficina Francisco Brennand, a stunning ceramics workshop and museum. Recife is also known for hosting one of Brazil’s most vibrant Carnival celebrations, where Frevo and Maracatu rhythms take over the streets in an explosion of color and energy.
            
            In the field of education and technology, Recife is a leading center for innovation in Brazil. The Porto Digital, one of the most advanced technology parks in Latin America, houses startups and research institutions specializing in IT, creative industries, and cybersecurity. The Federal University of Pernambuco (UFPE), founded in 1946, is one of the country’s top universities, contributing to Recife’s reputation as a center of academic excellence.
            
            With a blend of history, culture, and innovation, Recife stands out as one of Brazil’s most fascinating cities, offering visitors a mix of breathtaking beaches, a rich artistic scene, and a dynamic technological environment.
        
                                        The Ground Zero is a large square with a beautiful view of the Capibaribe River and the city skyline. It is a popular meeting point for locals and tourists alike, and it often hosts cultural events, concerts, and fairs. The square is also home to a large map of Recife, which shows the main tourist attractions in the city.
                                        The city center is also known for its lively atmosphere, with street vendors, shops, and restaurants offering a variety of local cuisine and handicrafts. Visitors can explore the narrow streets, admire the architecture, and experience the unique blend of old and new that characterizes Recife.
                                        The city is also known for its lively Carnival celebrations, where traditional music and dance fill the streets. Visitors can explore the many churches, museums, and art galleries that showcase the rich history and culture of Olinda.
                                        The area is also home to a variety of restaurants, shops, and accommodations, making it a popular spot for both locals and tourists. Porto de Galinhas is a great place to relax, enjoy water sports, and experience the local culture.
                                        The area is also home to many restaurants, bars, and shops, making it a popular destination for both locals and tourists. Boa Viagem Beach is a great place to relax and enjoy the sun while experiencing the lively culture of Recife.
                                        The complex is known for its stunning architecture, which combines elements of medieval castles with modern design. The Ricardo Brennand Institute is a popular destination for art lovers and tourists alike, offering a unique glimpse into the rich cultural heritage of Brazil.
                                        The atelier features a stunning collection of Brennand's work, set in a beautiful garden filled with sculptures and fountains. Visitors can explore the workshop, learn about the artistic process, and admire the intricate designs and vibrant colors of Brennand's ceramics.
                                        The area is also home to a variety of restaurants and accommodations, making it a popular destination for both locals and tourists. Carneiros Beach is a great place to unwind and enjoy the natural beauty of northeastern Brazil.
                                        The center features exhibitions, workshops, and performances that celebrate the history and significance of Frevo in Brazilian culture. Visitors can learn about the dance's origins, its vibrant costumes, and its role in the city's Carnival celebrations.
                                        CETENE, or the Centre for Strategic Technologies of the Northeast (Centro de Tecnologias Estratégicas do Nordeste), is a research and development institution whose primary focus is promoting technological innovations and advancements in strategic sectors, including health, energy, and sustainable development. It plays a significant role in fostering collaboration between government, academia, and industry to address regional challenges and enhance technological capacity in Northeast Brazil. It is situated in the University City (Cidade Universitaria) neighbourhood near the UFPE campus.
Here are some hotel recommendations in the city of Recife, with options for different profiles.
            Transamerica Prestige Recife
            Avenida Boa Viagem, 420 Boa Viagem - Recife/PE CEP: 51011-000
            Phone: +55 81 3039 9000
            Discount coupon: SBMF2025
            Website: https://www.letsatlantica.com.br/hotel/transamerica-prestige-beach-class
        
            Radisson Recife 
            Av. Boa Viagem, 1906. Boa Viagem. Recife - PE
            Phone: +55 81 3126 3020
            Discount coupon: SBMF (for stays between 29/11 and 05/12)
            Website: https://www.letsatlantica.com.br/hotel/radisson-recife
        
            Ibis Recife Boa Viagem 
            Av. Domingos Ferreira 683, Boa Viagem, Recife
            Phone: +55 81 3334 3434
            Website: https://all.accor.com/hotel/6000/index.pt-br.shtml
        
            Ibis Recife Aeroporto 
            Av. Mal. Mascarenhas de Morais - Imbiribeira, Recife - PE
            Phone: +55 81 3201 8700
        
            Uzi Praia Hotel 
            Av. Conselheiro Aguiar, 942 - Boa Viagem, Recife - PE
            Phone: (81) 97100-2264
        
            Marante Plaza Hotel 
            Av. Boa Viagem, 1070 - Boa Viagem, Recife - PE
            Phone: +55 81 3464 1070
        
The conference dinner will be held at the Entre Amigos Praia on Thursday, December 4th, at 7:30 PM.