Gustavo Carvalho (Federal University of Pernambuco)

Formal methods: what are they? What are they used for?

Lecture slides: click here.

In this talk, we provide an example-based introduction to formal methods by covering different notations and languages (namely, the B language, the CSP process algebra, the SMT-LIB language, the Gallina specification language, and timed automata) that enable reasoning about data, time, and concurrency properties. We also discuss tool support (namely, Atelier B, ProB, BMotionWeb, FDR4, UPPAAL, Z3, and Coq) for animation, visualisation, interactive and automated verification, and code generation.

Lucas Cordeiro (The University of Manchester and Federal University of Amazonas)

Securing Software Systems: Exploring Automated Testing, Verification, and Synthesis Strategies

Lecture slides: click here.

In this talk, I'll delve into automated testing, formal verification, and synthesis techniques that establish a robust foundation for building secure software systems. We'll begin by exploring security concepts, demystifying traditional notions and vulnerabilities unique to low-level software systems. Building on this, we'll dive into cutting-edge methods, covering state-of-the-art testing, verification, and synthesis techniques. This dynamic spectrum spans fuzzing, model checking, constraint programming, and abstract interpretation for vulnerability detection. We'll also touch on counterexample-guided inductive synthesis and leveraging large language models for root cause analysis and program repair. Lastly, I'll showcase recent achievements highlighting a hybrid approach for safeguarding against memory safety and concurrency vulnerabilities in low-level software systems. This forward-looking approach employs a logic-based automated reasoning framework, thoughtfully examining search, learning, memory, and parallelization aspects. Throughout the talk, practical examples will bring concepts to life, spanning scenarios such as inspecting firmware security vulnerabilities in modern processors and ensuring the integrity of communication protocols and embedded control software in drone technology.

Poster Session

SBMF 2023 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 Haniel Barbosa (hbarbosa@dcc.ufmg.br).

The deadline for posters submission is Oct 27, 2023. The notification will be sent to authors Nov 6, 2023.

Presented Posters

Carcara: A proof checker and elaborator for SMT proofs

Bruno Andreotti, Haniel Barbosa

Poster: click here.

Towards a Neurosymbolic Approach to the Weighted model Counting

Adriel Santos, Luca Naja, Matheus Uchôa, Edjard Mota

Poster: click here.

Towards a neurosymbolic approach to the MAX-SAT problem using LBM

Kristian Aguilar, Gustavo Oliveira, Jônatas Lima, Fernando Ventilari, Edjard Mota

Poster: click here.

Financial Support

SBMF will provide partial support for a limited number of students attending ETMF 2023. If you want to apply, please get in contact via an e-mail to: edjard@icomp.ufam.edu.br, hbarbosa@dcc.ufmg.br.