ETMF 2025
10th School of Theoretical Computer Science and Formal Methods
December 2nd, 2025
Recife / Brazil
Recife / Brazil
The 10th edition of the School of Theoretical Computer Science and Formal Methods (ETMF 2025) is a co-located event of SBMF 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:
Abstract: Correctness is not a luxury—it is a necessity for dependable software systems. Yet, testing alone can never prove that a program always behaves as intended. The Design by Contract principle offers a pragmatic way to bridge programming and formal reasoning, by making software specifications explicit and checkable. This mini-course introduces the Java Modeling Language (JML) and the OpenJML verification tool through a hands-on, example-driven journey. Participants will learn how to specify contracts, invariants, and loop properties, and how to use OpenJML to automatically verify that Java implementations respect these specifications. Beyond the technical aspects, the course aims to inspire a mindset shift: that formal verification is not an abstract academic exercise, but a practical and empowering technique for programmers who want to make their code provably trustworthy. By the end, participants will be able to write Java programs with precise contracts and use OpenJML to verify that these contracts are correctly implemented.
Abstract: This course introduces participants to essential formal verification techniques for hardware projects using Cadence Jasper, the industry-leading platform for formal verification. Participants will learn fundamental concepts of hardware functional verification and basic principles of formal verification methodologies using the market's most advanced solutionS. The curriculum covers key topics including SystemVerilog Assertions (SVA) language for property specification, Sequential Equivalence Checking (SEC) for design comparison, and an introduction to formal verification methodologies. Students will have direct contact with the tool's main functionalities through guided practical exercises. Participants will also be introduced to the tool's C/C++ capabilities and learn basic concepts for verification between C/C++ models and RTL implementations. By the end of this course, participants will have the initial knowledge needed to begin exploring formal verification in the hardware development world.
ETMF 2025 will take place at the Informatics Centre (Centro de Informática -- CIn) of the Federal University of Pernambuco (Universidade Federal de Pernambuco -- UFPE). It is one of the most well-known informatics centers in Brazil as well as in Latin America. Many of the country’s most qualified workforce in Information Technology (IT) comes from here. Many successful IT companies begun as startups at the Center. Also, through partnerships with the private sector, CIn-UFPE has a strong national and international presence in research and education in informatics.
