The 9th edition of the School of Theoretical Computer Science and Formal Methods (ETMF 2024) is a premier event dedicated to advancing knowledge in the field of theoretical computer science and the application of formal methods to software and system development. ETMF provides an educational forum where researchers, students, and professionals from academia and industry can exchange ideas, learn about the latest developments, and explore practical applications of formal methods in various domains.
The school features a series of lectures, tutorials, and hands-on sessions delivered by renowned experts in the field, covering both foundational topics and cutting-edge research. Topics span a wide range of areas, including but not limited to:
ETMF 2024 is organized by the Graduate Program in Applied Computing (PPComp) at the Federal Institute of Espírito Santo (Ifes) and will take place in Serra, a city known for its growing industrial base and natural beauty. The event aims to foster collaborations between researchers and practitioners, strengthen the formal methods community, and inspire future research that meets contemporary technological challenges.
In this lecture, we will explore the fundamentals of TLA+ (Temporal Logic of Actions), a formal specification language used for modeling and verifying complex systems. TLA+ is particularly powerful for specifying concurrent and distributed systems, ensuring correctness in system design. Participants will be introduced to the core concepts of TLA+, including temporal logic, behaviors, and invariants, along with practical examples of system specifications using TLA+. This session is ideal for those interested in understanding how to leverage formal methods for rigorous system design and verification.
About the speaker: Prof. Dr. Jefferson O. Andrade holds a Bachelor's in Computer Engineering and a Master's in Computer Science from the Federal University of Espírito Santo (UFES), as well as a PhD in Education. He is a Professor at the Federal Institute of Espírito Santo (Ifes) and a member of the Applied Computing Graduate Program (PPComp). His research is focused on formal methods and system verification, with a strong collaboration with the University of Tsukuba in Japan. He specializes in multi-valued logics, probabilistic verification, and developing toolchains for safety-critical systems. Prof. Andrade also has substantial experience in applied research, including collaboration with steel and mining industries. He leads projects that combine formal methods research with industrial challenges, bridging theory and practice effectively.
Formal methods are crucial for ensuring software correctness, safety, and security, but they are only part of the broader engineering process. The presentation provides a comprehensive overview of the role of formal methods in ensuring the safety and security of software-based systems in critical industries. A few concrete examples from the world of railways will help you to understand the added value of formal methods, but also to identify anything that needs to be dealt with in a more traditional way. Notation is introduced during the talk. No other knowledge than mathematical logic and common sense are required to attend this lecture.
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.
This tutorial emphasizes the importance of timing in safety-critical systems like autonomous vehicles, traffic control, and railway management, where timely actions are essential for safe operation. It introduces **timed automata**, a mathematical model that integrates timing into traditional automata theory, allowing engineers to design and verify real-time systems. Using a train crossing example, participants will model systems with critical timing constraints and engage in hands-on exercises with UPPAAL, a tool for modeling and verifying timed systems. The tutorial combines theoretical foundations with practical applications, guiding participants to ensure system correctness and prevent timing violations that could endanger safety.
About the speaker: Dr. Ciprian Teodorov is an Full Professor at ENSTA Bretagne in Brest, France. He specializes in formal methods, model-driven engineering, and safety-critical systems. His research focuses on the use of formal techniques for verifying and validating the behavior of embedded systems, especially in safety-critical domains like transportation and aerospace. Dr. Teodorov has extensive experience in the application of formal methods to real-world problems, including system design and certification processes. He has contributed to various projects involving system modeling, formal verification, and the development of toolchains for ensuring system reliability and safety.
| Time | Activity | Room |
|---|---|---|
| 08:30 - 09:00 | Registration | Entrance hall |
| 09:00 - 09:30 | ETMF Opening Ceremony | Auditorium |
| 09:30 - 10:30 | ETMF – Mini-course 1 (Jefferson Andrade) | Lab. 208 |
| 10:30 - 11:00 | Coffee Break | Block 5 |
| 11:00 - 12:30 | ETMF – Mini-course 1 (Jefferson Andrade) | Lab. 208 |
| 12:30 - 14:30 | Lunch | |
| 14:30 - 16:00 | ETMF – Mini-course 2 (Thierry Lecomte) | Lab. 208 |
| 16:00 - 16:30 | Coffee Break | Block 5 |
| 16:30 - 17:30 | ETMF – Mini-course 3 (Ciprian Teodorov) | Lab. 208 |
| 17:30 - 18:00 | ETMF Closing Ceremony | Auditorium |
All ETMF 2024 activities will take place at IFES – Campus Serra.
See the complete SBMF 2024 program.
ETMF 2024 will have a poster session from students attending ETMF who want to submit a poster. The posters are intended for descriptions of works in progress, student projects and relevant research being published elsewhere. Submissions should be in English, in the form of at most one page abstract, CEURART format containing title and authors name with affiliation. The files should be sent directly to Jefferson Andrade <jefferson.andrade@ifes.edu.br>.
The list of selected posters for the 9th School of Theoretical Computer Science and Formal Methods (ETMF 2024) will be made available on November 6, 2024. Please check back on this date for the official selection.
Ifes, Campus Serra
Av. dos Sabiás, 330 - Morada de Laranjeiras,
Serra - ES, 29166-630
ETMF 2024 will be held at the Serra Campus of the Federal Institute of Espírito Santo (Ifes). Located in the thriving city of Serra, the campus serves as a center for cutting-edge research and innovation, particularly in the fields of applied computing and technology. It is home to the Graduate Program in Applied Computing (PPComp), which plays a pivotal role in hosting this prestigious event.
The Ifes Campus Serra is known for its modern facilities and academic excellence, fostering an environment conducive to learning, collaboration, and intellectual exchange. The event will take place in state-of-the-art lecture halls and research spaces, providing attendees with a comfortable and inspiring setting to engage with the latest developments in theoretical computer science and formal methods.
Situated within easy reach of Vitória, the capital of Espírito Santo, the campus offers convenient access to both urban amenities and the natural beauty of the region, making it an ideal location for ETMF 2024.
Serra, the most populous municipality in Espírito Santo, is located just 27 km north of Vitória, in the Greater Vitória metropolitan area. Known for its unique combination of natural beauty and modern urban development, Serra is home to the iconic Mestre Álvaro, one of the largest coastal elevations in Brazil, offering breathtaking views of the region and rich biodiversity. This volcanic massif stands as a symbol of the city’s deep connection to nature, making Serra an excellent destination for eco-tourism enthusiasts.
Beyond its natural wonders, such as the beaches of Jacaraípe and Manguinhos, which are famous for their tranquil fishing villages and annual events, Serra is also a growing commercial and industrial hub. The municipality plays a key role in the state's economic development, with a strong presence in retail and industry.
Hosting the 9th School of Theoretical Computer Science and Formal Methods (ETMF 2024) is the Serra Campus of the Federal Institute of Espírito Santo (Ifes). The campus is home to the Graduate Program in Applied Computing (PPComp), which stands out for its contributions to research and innovation in the field of applied computing. PPComp plays a critical role in training highly qualified professionals and conducting research that addresses contemporary demands in technology and society.
The event will foster knowledge exchange and innovation in a city that blends modernity, tradition, and academic excellence.
Below are the bus lines that connect Vitória to Ifes Campus Serra:
These bus routes make it convenient for those traveling from Vitória to reach Ifes Campus Serra.
For attendees of the ETMF 2024 event, there are several hotel options available in Serra, catering to a range of preferences and budgets. Whether you're seeking accommodations near the event venue for convenience or more affordable options in nearby neighborhoods, you'll find suitable choices.
If you are planning to attend both ETMF 2024 and SBMF 2024, we recommend referring to the SBMF 2024 Hotels section for additional hotel recommendations in Vitória, which may offer better convenience for attending both events.
Serra Linda Hotel
R. dos Uirapurús, 559 - Morada de Laranjeiras, Serra - ES, 29166-710
Telefone: +55 (27) 3338-7538
Serra Grande - Hotel & Churrascaria
Av. Eldes Scherrer Souza, 870 - Parque Res. Laranjeiras, Serra - ES, 29165-680
Telefone: +55 (27) 2125-5200
Hotel Jardins
ES-010, 1307 - Jardim Limoeiro, Serra - ES, 29164-140
Telefone: +55 (27) 3298-9800
