The Brazilian Symposium on Formal Methods (SBMF) is a scientific event that has been held annually since 1998. The 27th edition of SBMF will take place in 2024 in Vitória, the capital of Espírito Santo. SBMF courses and lectures are dedicated to disseminating recent advances in the field of formal methods. The technical sessions of SBMF foresee the presentation of unpublished works that make clear and significant contributions to the state of the art in the theory and practice of formal methods.
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
This keynote explores how formal methods can be seamlessly integrated into software development tools, allowing developers to benefit from increased system reliability and safety without needing expertise in formal verification techniques. Two examples are presented: 1) automatic transformation of SysADL architecture descriptions into formal specifications for verification, and 2) a method for modeling Relay-based Railway Interlocking Systems in CSP to verify critical safety properties. Both examples showcase how user-friendly tools can "hide" the complexity of formal methods while still delivering their powerful benefits to "Muggles" (non-experts).
About the speaker: Marcel Vinicius Medeiros Oliveira is a Full Professor at the Department of Informatics and Applied Mathematics at the Federal University of Rio Grande do Norte (UFRN). He holds a Ph.D. in Computer Science from the University of York, England, and specializes in Formal Methods, with research focusing on refinement calculus, concurrency, formal language semantics, and code synthesis from formal specifications. Marcel is also a member of various academic committees, including the National Institute for Software Engineering, and serves as Coordinator of Technical Courses at UFRN’s Digital Metropolis Institute. His teaching covers Databases, Logic Applied to Software Engineering, and Formal Methods.
This keynote recounts a 15-year journey by the Kairos team to address the growing complexity of software-intensive systems. Focusing on the use of Software Language Engineering for formalizing model-based systems engineering, the talk will explore challenges such as ensuring consistency between heterogeneous models, formalizing model correspondences, and automating model coordination. The team's work on developing formal, language-agnostic methods and new metalanguages for tool automation will be highlighted, offering valuable insights into the evolution of formal systems engineering.
About the speaker: Julien Deantoni is a Professor at the Université Côte d'Azur and a researcher with the I3S/INRIA KAIROS team. His research focuses on the development of domain-specific languages (DSLs), particularly in the context of modeling and simulation of complex systems, behavioral semantics, and concurrent system coordination. He has contributed significantly to the development of tools such as TimeSquare, which allows for the specification and analysis of logical time constraints using the Clock Constraint Specification Language (CCSL). Julien has led various European and national research projects, including work on co-simulation frameworks for cyber-physical systems. His teaching covers a wide range of topics, including finite state machines, C++ programming, and embedded systems.
In deductive verification and software model checking, dealing with certain language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. This applies, in particular, to the concept of extended quantifiers found in specification languages like JML and ACSL. Extended quantifiers can be used to compute, among others, the maximum element or the sum of elements of an array and are frequently used in specifications, but tend to be difficult to support in verification tools. In the talk, I will present our ongoing research on how to automatically transform programs with such complicated operators to equivalent programs not containing the operators, and to reason about the correctness of those simpler programs instead. We apply our framework to cover the different kinds of extended quantifiers, which we formalize as monoid homomorphisms. Our approach is generic, however, and can be applied to describe a wide range of program transformations. The presentation is based on joint work with Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Marten Voorberg.
About the speaker: Philipp Rümmer is a Professor of Theoretical Computer Science at the University of Regensburg and also serves as a Senior Lecturer at Uppsala University's Department of Information Technology. His research spans theorem proving, SAT/SMT solving, and decision procedures, with a strong focus on program analysis for languages such as Java, C#, C, C++, and Simulink. He is also involved in the modeling and analysis of timed, parameterized, and concurrent systems, employing methods like deductive verification, model checking, and automatic test case generation. Additionally, Philipp explores the intersection of machine learning, automata learning, and artificial intelligence with verification processes, and has contributed to the verification of embedded systems and software.
In this presentation, we explore whether formal methods serve as allies or obstacles to industrial progress. Building upon insights presented at SBMF 2019, we delve into the evolving landscape of formal verification and validation, and its industrial integration. The technological landscape has evolved considerably, particularly regarding cybersecurity and artificial intelligence (AI). The surge in cybersecurity threats, now more advanced than before, requires robust formal verification to assess system resilience against sophisticated attacks. Modeling tools have become vital assets against these threats. Moreover, AI's proliferation into areas such as autonomous mobility brings unique challenges that intersect with safety and reliability—fields traditionally addressed by formal methods. We assess whether these methods can adequately accommodate AI's dynamic, data-driven nature or if they present hurdles for certification and safety validation. Our experience over the past five years offers a comprehensive overview of what has worked, what has not, and sometimes how the relationship between industry and academia has evolved in the face of these new challenges. We provide practical insights, emerging synergies, and the critical role of formal methods in shaping the future of secure, reliable technology.
About the speaker: With 30 years of experience in R&D, Thierry Lecomte has worked on industrial projects in the automotive, healthcare, microelectronics, nuclear energy, railway and space industries. Today he is R&D director of CLEARSY, a French SME specialized in the invention of safety critical systems, where he has worked since its creation in 2001. His current subjects of interest are safety and security co-engineering, safe artificial intelligence, and autonomous mobility - all related to formal methods.
Formal methods are known for being rigorous and useful to verify specific parts of critical software. One of the main reasons it is still not considered to be mainstream in software is because of the high computational effort it requires. This presentation will go through an overview of the hardware verification process, explain how formal is largely used by companies that design state-of-the-art chips, and how Jasper overcame problems with scalability and the non-stop growth of the circuits that need to be verified, becoming the market leader in the formal world, and being widely used in the industry.
About the speaker: Rafael Hamdan has a BSc. from UFMG at Electrical Engineering with emphasis on Computer Science. Started software development in the early years of the century, when he was 10 years old, mainly with PHP and technologies that involved web development (JavaScript, SQL, HTML/CSS). Later, started learning new programming languages like C++ and C#, contributing for several years to OpenTibia – an open-source server written in C++ for an MMORPG – and other projects related to it. Joined Cadence Design Systems right after concluding his BSc. in 2017, and since then has worked in different areas under the R&D team of Jasper, including: HDL synthesis, HDL modeling for formal analysis, graph theory, parallelization, SEC (sequential equivalence checking), Coverage analysis and others. He currently manages the R&D teams responsible for the development of Coverage (COV) and UNR Apps from Jasper, which is the main formal verification tool in the EDA industry.
| Paper submission deadline†‡ | 18th August, 2024 5th July, 2024 |
| Acceptance notice | 23th September, 2024 6th September, 2024 |
| Camera-ready copy deadline† | 13th October, 2024 11th October, 2024 |
| SBMF 2024 | 4th—6th December, 2024 |
† All deadlines are until midnight of the specified date Anywhere on Earth (AoE).
‡ This is the final submission deadline and there will be no further extensions.
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).
| Dates | Category | SBMF | SBMF + SBC membership |
|---|---|---|---|
| 12/Aug - 29/Sep | Undergraduate Student – SBC Member | R$ 63,00 | R$ 94,00 |
| Undergraduate Student – non SBC Member | R$ 101,00 | R$ 94,00 | |
| Graduate Student – SBC Member | R$ 118,00 | R$ 243,00 | |
| Graduate Student – non SBC Member | R$ 255,00 | R$ 243,00 | |
| Basic Education Teacher – SBC Member | R$ 165,00 | R$ 290,00 | |
| Basic Education Teacher – non SBC Member | R$ 307,00 | R$ 290,00 | |
| Professional – SBC Member | R$ 211,00 | R$ 567,00 | |
| Professional – non SBC Member | R$ 589,00 | R$ 567,00 | |
| 30/Sep - 03/Nov | Undergraduate Student – SBC Member | R$ 88,00 | R$ 119,00 |
| Undergraduate Student – non SBC Member | R$ 128,00 | R$ 119,00 | |
| Graduate Student – SBC Member | R$ 134,00 | R$ 259,00 | |
| Graduate Student – non SBC Member | R$ 273,00 | R$ 259,00 | |
| Basic Education Teacher – SBC Member | R$ 180,00 | R$ 305,00 | |
| Basic Education Teacher – non SBC Member | R$ 323,00 | R$ 305,00 | |
| Professional – SBC Member | R$ 227,00 | R$ 583,00 | |
| Professional – non SBC Member | R$ 606,00 | R$ 583,00 | |
| 04/Nov - 06/Dec | Undergraduate Student – SBC Member | R$ 103,00 | R$ 134,00 |
| Undergraduate Student – non SBC Member | R$ 145,00 | R$ 134,00 | |
| Graduate Student – SBC Member | R$ 149,00 | R$ 274,00 | |
| Graduate Student – non SBC Member | R$ 289,00 | R$ 274,00 | |
| Basic Education Teacher – SBC Member | R$ 196,00 | R$ 321,00 | |
| Basic Education Teacher – non SBC Member | R$ 341,00 | R$ 321,00 | |
| Professional – SBC Member | R$ 237,00 | R$ 593,00 | |
| Professional – non SBC Member | R$ 617,00 | R$ 593,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 2nd of December.
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 2024. Authors can not use the registration benefits (exemption or 50% discount) granted by SBC to affiliated institutions. The author registration must be paid until November 11th, 2024.
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 on the basis of 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=sbmf2024
The proceedings of SBMF 2024 will be published as part of Springer's Lecture Notes in Computer Science series. Conference participants will have free access to the proceedings from December 1, 2024, to January 15, 2025, via the following link: https://link.springer.com/book/9783031781155.
Presentation Durations:
The award for best paper was given to the article "Verifying integrated designs of UML state machines and activities using CSP" by Diego Ferreira and Lucas Lima.
| Time | Tuesday (2024-12-03) | Wednesday (2024-12-04) | Thursday (2024-12-05) | Friday (2024-12-06) |
|---|---|---|---|---|
| 08:30 | Registration Ifes Serra, Entrance hall | Registration Innovation City, Entrance hall | Registration Innovation City, Entrance hall | Registration Innovation City, Entrance hall |
| 09:00 | ETMF Opening Ceremony Ifes Serra, Auditorium | Meet and Greet Innovation City, Entrance hall | Keynote: Julien Deantoni Innovation City, Conference room | Keynote: Philipp Rümmer Innovation City, Conference room |
| 09:30 | ETMF – Mini-course 1 (Jefferson Andrade) Ifes Serra, Lab. 208 | |||
| 10:00 | Coffee Break Innovation City, Living area | |||
| 10:30 | Coffee Break Ifes Serra, Block 5 | BSB Keynote: Giancarlo Guizzardi Innovation City, Conference room | Coffee Break Innovation City, Living area | Coffee Break Innovation City, Living area |
| 11:00 | ETMF – Mini-course 1 (Jefferson Andrade) Ifes Serra, Lab. 208 | Technical Session #2 Innovation City, Conference room | Industrial Session Innovation City, Conference room | |
| 11:30 | Lunch | |||
| 12:00 | ||||
| 12:30 | Lunch | Lunch | Lunch | |
| 13:00 | ||||
| 13:30 | Registration Innovation City, Entrance hall | |||
| 14:00 | SBMF Opening Ceremony Innovation City, Conference room | |||
| 14:30 | ETMF – Mini-course 2 (Thierry Lecomte) Ifes Serra, Lab. 208 | Keynote: Marcel Oliveira Innovation City, Conference room | Technical Session #3 Innovation City, Conference room | Technical Session #4 Innovation City, Conference room |
| 15:00 | ||||
| 15:30 | ||||
| 16:00 | Coffee Break Ifes Serra, Block 5 | Coffee Break Innovation City, Living area | Coffee Break Innovation City, Living area | SBMF Closing Ceremony Innovation City, Conference room |
| 16:30 | ETMF – Mini-course 3 (Ciprian Teodorov) Ifes Serra, Lab. 208 | Technical Session #1 Innovation City, Conference room | CEFM Meeting Innovation City, Conference room | Closing Cocktail Innovation City, Living area |
| 17:00 | ||||
| 17:30 | ETMF Closing Ceremony Ifes Serra, Auditorium | |||
| 18:00~19:30 | ||||
| 20:00 | Conference Dinner Barlavento Beach Bar & Lounge | |||
| 20:30 | ||||
| 21:00 | ||||
| 21:30 | ||||
| 22:00 | ||||
| 22:30 |
Vitória, the capital of Espírito Santo, located in the Southeast
region of Brazil, is known for its beautiful beaches, historical
heritage, and strong economy. The city is a major financial,
corporate, research, technology, entertainment, and commercial
center in Brazil. Situated on an island, Vitória is famous for the
combination of its natural beauty with a vibrant urban life.
Hosting the 27th Brazilian Symposium on Formal Methods (SBMF 2024)
is the Graduate Program in Applied Computing (PPComp) at the Serra
Campus of the Federal Institute of
Espírito Santo (Ifes). Ifes is known for its excellence in
technical and higher education, offering a wide range of programs
across various fields of knowledge. PPComp, in particular, stands
out for its contribution to research and innovation in the field of
Applied Computing, being a pillar in the training of highly
qualified professionals and in conducting research that meets the
contemporary demands of society and the market.
Launched in 2019, PPComp is a young program that actively seeks to
consolidate itself as a center of excellence in its area. With a
firm commitment to the quality of education and research, the
program is committed to significantly contributing to the
advancement of applied computing, developing a solid foundation to
become a benchmark in the future, both regionally and nationally.
Moreover, the program's faculty have been actively collaborating
with local companies on research and technological development
projects, strengthening the bridge between academia and the
industrial sector, and contributing to the region's economic and
technological development.
The 27th SBMF will be hosted at the "Cidade da Inovação" (Innovation City) of Ifes, a hub designed to foster transformative solutions for sustainable development through collaboration with governmental bodies, the industrial sector, and civil society. Situated in the Jardim da Penha neighborhood of Vitória, in the premises formerly known as the IBC Sheds, this space now houses the Vitória Innovation Hub (PEIF-IFES), focusing on research and innovation in metallurgy, materials, and AI, alongside the regional office of the National Institute of Industrial Property (INPI).
The ambition is for this location to not only serve as a physical site for innovation and collaboration but to also act as a platform connecting the Ifes community, local society, and the productive sector globally.
Here are some hotel recommendations in the city of Vitória, catering to various preferences. For attendees seeking convenience, there are accommodations near the "Cidade da Inovação". For those looking for value, several budget-friendly options are available throughout the city.
ibis Vitoria Praia de Camburi
Av. Dante Michelini, 791 - Praia De Camburi, Vitória - ES, 29060-235
Telefone: +55 (27) 3203-5450
Vitória Praia Hotel
Av. Dante Michelini, 1057 - Jardim da Penha, Vitória - ES, 29060-235
Telefone: +55 (27) 3010-5500
Hotel Sol da Praia
Av. Dante Michelini, 877 - Jardim da Penha, Vitória - ES, 29065-050
Telefone: +55 (27) 2127-1500
Alameda Vitória Hotel
Av. Dante Michelini, 585 - Jardim da Penha, Vitória - ES, 29060-235
Telefone: +55 (27) 3204-6600
Ibis Budget Vitoria
Av. Nossa Sra. da Penha, 1993 - Bela Vista, Vitória - ES, 29056-075
Telefone: +55 (27) 3205-6155
Hotel Minuano
Avenida Dantas Micheline, 337 - Camburi, Vitória - ES, 29060-235
Telefone: +55 (27) 2121-7877
Ibis Vitoria Aeroporto
BR-101, Km 2 - S/2 - Bairro Carapina, Serra - ES, 29161-793
Telefone: +55 (27) 3041-4900
