O aluno de mestrado do Programa de Pós-graduação em Ciência da Computação (PPGCC) da UFMG, Bruno Anderotti, apresentou um trabalho científico na conferência internacional Verification, Model Checking, and Abstract Interpretation (VMCAI 2026), realizada nos dias 12 e 13 de janeiro/26, em Rennes, na França. O estudo foi desenvolvido no Departamento de Ciência da Computação (DCC) da universidade, com orientação do professor Haniel Moreira Barbosa.
Na conferência, o estudante apresentou o artigo intitulado “Producing Shorter Congruence Closure Proofs in a State-of-the-Art SMT Solver”, resultado de uma pesquisa conduzida em parceria com seu orientador. O trabalho integra o projeto de mestrado de Bruno e foi desenvolvido no grupo de pesquisa SMITE, dedicado ao estudo de métodos formais e ferramentas de verificação automática.
A pesquisa propõe a implementação de novos algoritmos no módulo de congruence closure do solucionador SMT cvc5, uma ferramenta amplamente utilizada na área de verificação formal. Esse módulo é responsável por raciocinar sobre equivalências entre termos e constitui um componente central para o funcionamento do solucionador. O objetivo do trabalho é produzir demonstrações mais curtas, contribuindo para maior eficiência e clareza nos processos de verificação automática.
A VMCAI é um evento internacional que reúne pesquisadores de diversos países interessados em temas como verificação formal, verificação de modelos (model checking) e interpretação abstrata. A edição de 2026 ocorreu em conjunto com a conferência Principles of Programming Languages (POPL), uma das mais relevantes na área de linguagens de programação e campos relacionados, ampliando o intercâmbio científico entre os participantes.
A participação no evento contou com apoio financeiro do PPGCC e do projeto PEGISUS, financiado pela agência de pesquisa estadunidense DARPA.
