Event Start

About

The Brazilian Symposium on Formal Methods (SBMF) is a scientific event that has been held annually since 1998. The 26th edition of SBMF will take place in 2023 in Manaus, the capital of Amazonas. 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



Schedule

Monday
(04/12/23)
Tuesday
(05/12/23)
Wednesday
(06/12/23)
Thursday
(07/12/23)
Friday
(08/12/23)
8:30 Registration / Opening Registration / Opening Registration Registration Registration
9:00 ETMF AFRiTS workshop Opening Cerimony Keynote: Chantal Industrial Talk: Felipe (AWS)
9:30 Keynote: Stéphane
10:00 Short break short break
10:30 Short break Short break Technical Session #2 Technical Session #3
11:00 ETMF Technical Session #1
11:30
12:00 Lunch Lunch
12:30 Lunch Lunch Lunch
13:00
13:30
14:00 Panel Keynote: Artur
14:30 ETMF AFRiTS workshop Poster session
15:00 Closing
15:30 Açaí break Açaí break -
16:00 Açaí break Açaí break Tutorial: Vince Business meeting -
16:30 ETMF AFRiTS workshop -
17:00 - -
17:30 - -
18:00 - - -
- - - - - -
20:00 - - - Conference dinner -


Technical Section #1: Specification and Modeling

  • Automated code generation for DES controllers modeled as Finite State Machines
  • A Haskell-embedded DSL for Secure Information-flow
  • ULKB Logic: A HOL-based framework for reasoning over knowledge graphs

Technical Section #2: Testing and Verification I

  • CSP Specification and Verification of a Relay-Based Rail Interlocking System
  • Language-based Testing for Pushdown Reactive Systems
  • Sound Test Case Generation for Concurrent Mobile Features

Technical Section #3: Testing and Verification II

  • A Formal Model for Startups Financial Transactions
  • AutomaTutor: An Educational Mobile App for Teaching Automata Theory
  • ESBMC v7.3: Model Checking C++ Programs using Clang

Panel: How is Artificial Intelligence influencing Formal Methods? Challenges and opportunities

In recent years, we all have witnessed an avalanche of AI techniques transforming our customary tasks, affecting several aspects of our lives, including the research and development of systems. In this panel, we plan to discuss how the current AI technology trend has impacted the formal methods field. Also, how formal methods can be applied to support the existing AI techniques to improve trustworthiness. Finally, we would like to debate limitations and barriers to integrating both areas, successful cases, and potential collaborations yet to be explored.

Special Talks

Invited speakers

Professor Artur d'Avila Garcez

City University of London

Title: Neurosymbolic AI to achieve Trustworthy AI


Professor at the City, University of London, a pioneer in Neuralsymbolic Artificial intelligence. His research interests include the integration of Neural Networks and symbolic Al, machine learning, knowledge representation and reasoning. He hypothesizes that neural-symbolic systems can develop better models of knowledge acquisition, robust learning and reasoning under uncertainty.

Professor Chantal Keller

Université Paris-Saclay

Title: Automated reasoning for Type theory


Professor at the Université Paris-Saclay. Her research interests include programming languages and formal methods, notably through Type Theory, the combination of automated and interactive provers, and proof and test of programs. She has been applying such methods to many domains from programming languages themselves to security.

Dr Stéphane Graham-Lengrand

Technical Director at SRI International

Title: Collaborating reasoners: theory combination beyond Nelson-Oppen


Technical Director of SRI International, one of the most renowned research institutes in Silicon Valley. He is an expert in automated reasoning and has made significant contributions to the development of methods for verifying correctness and security aspects of computational systems.

Tutorial

Vince Molnár

PhD, Assistant Professor at BME-FTSRG

Formal Methods in Systems Engineering - Verifying SysML v2 Models


Vince Molnár is an assistant professor at the Budapest University of Technology and Economics, Hungary. His main research field is model-based development and formal methods, with the primary focus on the design and verification of safety-critical systems. He is the leader of the development of the Gamma Statechart Composition Framework. He was a member of the SysML v2 Submission Team and is now chairing the Conformance and Formal Methods Working Groups of OMG's Systems Modeling Community. He is an active member of the Semantics and Execution Working Groups as well.

Industrial talk

Felipe R. Monteiro

Applied Scientist at Amazon Web Services (AWS)

Model Checking in the Software Development Workflow at AWS


Felipe R. Monteiro is an Applied Scientist with the Automated Reasoning Group at Amazon. His main experiences are in static analysis, model checking, and software verification. His most recent work combines compositional techniques with model checking to verify complex software systems.

Important Dates

28th July, 2023 11th August, 2023 Paper submission deadline
8th September, 2023 15h September, 2023 Acceptance notice
9th October Camera-ready copy deadline
4th to 8th of December SBMF 2023

Registration

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

Registration is on!

Choose from the table below how do you plan to participate and then click here to register!

* AFRiTS and ETMF are additional activities.

** Full discount at AFRiTS and EMTF exclusively for undergraduate students.

*** Extended academic Black Friday with first batch values.



Event Categories SBMF
(R$)
AFRiTS*
(R$)
ETMF*
(R$)
SBMF+AFRiTS*
(R$)
SBMF+ETMF*
(R$)
SBMF+AFRiTS*+ETMF*
(R$)
14 sep - 15 oct Professional – SBC Member 175 50 50 225 225 275
Professional – non SBC Member 311 50 50 361 361 411
Graduate Student – SBC Member 130 50 50 180 180 230
Graduate Student – non SBC Member 262 50 50 312 312 362
Undergraduate Student – SBC Member 85 0** 0** 85** 85** 85**
Undergraduate Student – non SBC Member 123 0** 0** 123** 123** 123**
16 oct - 16 nov Professional – SBC Member 190 70 70 260 260 330
Professional – non SBC Member 328 70 70 398 398 468
Graduate Student – SBC Member 145 70 70 215 215 285
Graduate Student – non SBC Member 278 70 70 348 348 418
Undergraduate Student – SBC Member 100 0** 0** 100** 100** 100**
Undergraduate Student – non SBC Member 139 0** 0** 139** 139** 139**
17 nov - 8 dec Professional – SBC Member 205 90 90 295 295 385
Professional – non SBC Member 344 90 90 434 434 524
Graduate Student – SBC Member 160 90 90 250 250 340
Graduate Student – non SBC Member 295 90 90 385 385 475
Undergraduate Student – SBC Member 85*** 0** 0** 85*** 85*** 85***
Undergraduate Student – non SBC Member 123*** 0** 0** 123*** 123*** 123***


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:

  • Access to the Eduroam wireless network;
  • Discount on enrollments in the more than 40 events held annually by SBC;
  • Differential enrollment fee in POSCOMP;
  • Access to studies conducted by SBC and intended for public or private agencies, expressing the Society's political positions.

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 8th 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 2020. 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 10th, 2023.

Until November 27th, it is possible to request an 80% refund of the registration fee paid for SBMF 2023. After this date, there will be no refund of any paid amount. This policy applies to both registration cancellation and the cancellation of any additional activities. To request a cancellation, please send your request to faturamento@sbc.org.br.

Committees

Program Committee

Papers

Accepted Articles

Conference proceedings can be accessed at the following link: Click here.

  • ULKB Logic: A HOL-based framework for reasoning over knowledge graphs
    Guilherme Lima, Alexandre Rademaker and Rosario Uceda-Sosa

  • [s] AutomaTutor: An Educational Mobile App for Teaching Automata Theory
    Steven Jordaan, Nils Timm and Linda Marshall

  • CSP Specification and Verification of a Relay-Based Rail Interlocking System
    P. E. R. Bezerra, M. V. M. Oliveira, Thierry Lecomte and D. I. de Almeida

  • Sound Test Case Generation for Concurrent Mobile Features
    Rafaela Almeida, Augusto Sampaio and Sidney C. Nogueira

  • A Haskell-embedded DSL for Secure Information-flow
    Cecilia Manzino and Gonzalo De Latorre

  • [s] ESBMC v7.3: Model Checking C++ Programs using Clang
    Kunjian Song, Mikhail Gadelha, Franz Brauße, Rafael Menezes and Lucas Cordeiro

  • A Formal Model for Startups Financial Transactions
    Rodrigo Stevaux and Ana de Melo

  • Automated code generation for DES controllers modeled as Finite State Machines
    Tiago Possato, João Valentini, Luiz Fernando Puttow Southier and Marcelo Teixeira

  • Language-based Testing for Pushdown Reactive Systems
    Adilson Bonifacio

Submission instructions (Closed)

We invite submissions of papers with a strong emphasis on formal methods, whether practical or theoretical, in the following categories:

  • Regular papers (limit of 15 pages). Proofs of theoretical results that do not fit the page limit may be provided in an appendix.
  • Short papers (limit of 8 pages). Short papers include system descriptions, user experiences, and case studies. We encourage authors to make the data needed to reproduce their experiments available.

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=sbmf2023

Manaus

Manaus, located on the banks of the Negro River in northwestern Brazil, is in the heart of the world's largest rainforest and is one of the biggest tourist destinations in Brazil. It is also the main financial, corporate, industrial, research, technology, entertainment, and commercial center of the Northern Region of Brazil. The city is situated at the confluence of the Negro and Solimões rivers, with the Teatro Amazonas listed as a National Historic Heritage by IPHAN its greatest cultural symbol.
Manaus was home to the first higher education institution in Brazil, founded on January 17, 1909. This originated from the defunct Free University of Manáos, which dismembered the Faculty of Law, forming the embryo of the current UFAM.
The Institute of Computing of the UFAM, which has only 30 years of history, is one of the two most important centers of higher education and research and entrepreneurship in computing startups in the North and Northeast of Brazil, being recognised as a postgraduate program of international level according to the most recent ranking by Capes, an agency of the Ministry of Education that promotes research and graduate studies.

Teatro Amazonas

The main cultural and architectural symbol of the state, Teatro Amazonas, located in Largo de São Sebastião in the heart of Manaus, keeps alive much of the history of the rubber boom, the golden age of the Amazonian capital. Inaugurated on December 31, 1896, the theater surprises and delights with its grandeur.

The concert hall seats 701 people, spread between the audience and three floors of boxes. It's impossible not to be mesmerized by the concave ceiling, which features four canvases painted in Paris by the renowned Casa Carpezot. The canvases depict music, dance, tragedy, and opera. In the center hangs a majestic French bronze chandelier. The masks on the columns of the audience, which pay tribute to composers and playwrights, are also noteworthy.

The Teatro Amazonas' boca cloth is another rarity. It was created in 1894 by Brazilian artist Crispim do Amaral and depicts the confluence of the Negro and Solimões rivers.

Nowadays, the theater hosts major events organized by the State Secretariat for Culture and Creative Economy, such as the Amazonas Opera Festival and the Dance and Theater festivals; high-brow performances like those presented by the State's Artistic and Cultural Bodies; and popular shows that benefit local artists of all genres.. More information (in portugues only) can be seen here.


Provincial Palace (Palacete Provincial)

The Provincial Palace houses three museums of different kinds: the Museum of Image and Sound (MISAM), the Museum of Numismatics of Amazonas, the Tiradentes Museum, the Pinacoteca do Estado, and the Archaeology Exhibition.

The building was founded in 1874 and served as the headquarters of the Military Police of Amazonas for more than 100 years. On March 24, 2005, it was transformed into a restaurant. However, it was reopened in 2009 as a museum, and the space is now open to the public free of charge. Visitors can come to learn about the collections and art of the museums, and the space also hosts cultural events that attract children, young people, and adults. Heliodoro Balbi Square (formerly Police Square), in front of the building, is an extension of the tour to the site.

The Pinacoteca has paintings, photos, and engravings by local, national, and international artists. The Museum of Numismatics has a collection of over 35,000 pieces and ancient coins. MISAM has DVDs and CDs that can be viewed for free on site. The Tiradentes Museum honors firefighters and state police, and exhibits weapons and uniforms. The Archaeology Exhibition reproduces excavations and artifacts discovered in the region.

Click here for more information

Event Location

The IComp, the venue of the 26th SBMF, is situated on the UFAM Campus which spans an area of about 600 hectares consisting of native and secondary forests, plateaus and floodplains, meadows, and deforested areas with plantations. Located on the east side of Manaus, the campus is enclosed by neighbourhoods and avenues.

Hotels

Here are some hotel recommendations in the city of Manaus, with options for different profiles. For those looking for a prime location, there are hotels near the UFAM. For those prioritizing value for money, there are more affordable options.

Location-based choices


Novotel Manaus
Av. Mandii, 4 - Distrito Industrial I, Manaus - AM, 69075-140
Telefone: (92) 2123-1211

Comfort Hotel Manaus
Av. Mandi, 263 - Distrito Industrial I, Manaus - AM, 69075-140
Telefone: (92) 3028-6056

Holiday Inn Manaus
Av. Rodrigo Otávio, 3721 - Japiim, Manaus - AM, 69073-177
Telefone: (92) 3182-0100

Trade-offs-based choices


Hotel ibis Manaus Distrito Industrial
Avenida Mandii 4 Distrito Industrial - Zona Industrial, Manaus - AM, 69075-140
Telefone: (92) 2123-6234

Seringal Hotel
R. Monsenhor Coutinho, 758 - Centro, Manaus - AM, 69020-230
Telefone: (92) 98179-2222

Boulevard Slaass Flat Hotel
Av. Alvaro Maia, 1445 - Praça 14 de Janeiro, Manaus - AM, 69020-210
Telefone: (92) 2129-5150

Bus lines to the campus

The UFAM offers three direct bus lines to the campus:

In addition, the Campus has an internal shuttle bus line between the Campus entrance and the North Sector, where the ICOMP - Institute of Computing is located. Line 007, known as "Integration" (or “Integração” in portuguese) is free and available to anyone.

Host and co-host organizers



Sponsorship