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.
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.
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.
Poster: click here.
Poster: click here.
Poster: click here.
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.
