Na última semana, o professor do Departamento de Ciência da Computação da Universidade Federal de Minas Gerais (DCC/UFMG), Haniel Moreira Barbosa, recebeu o prêmio de “SCP Best Tool Paper”, na ETAPS 2022. O evento reúne algumas das principais conferências internacionais em áreas relacionadas à software. Em particular, o artigo denominado “cvc5: A Versatile and Industrial-Strength SMT Solver”, foi apresentado na conferência TACAS 2022, uma das duas principais conferências da área de verificação
formal.
Segundo o professor, cvc5 é a mais nova iteração de solucionadores SMT (satisfatibilidade módulo teorias), na série de “cooperating validity checkers” (cvc), e estende a bem-sucedida base de código do anterior CVC4. “O artigo é uma descrição de sistema completa para a arquitetura do cvc5, além de destacar as principais novas funcionalidades e componentes desde o lançamento do CVC4 1.8. O artigo também apresenta uma avaliação do desempenho do cvc5 em todos os problemas da biblioteca SMT-LIB (padrão para avaliação de solucionadores SMT, com muitos dos problemas vindos de aplicações industriais), além de comparações com os solucionadores SMT CVC4 e Z3”, explicou.
Haniel contou que SMT é o problema de determinar a satisfatibilidade de uma fórmula lógica de primeira ordem de acordo com teorias lógicas. “Exemplos de teorias de interesse são diferentes formas de aritmética, como linear ou não-linear de inteiros ou de reais, além de vários tipos de dados, como: arrays, strings, listas, conjuntos, etc. Os solucionadores SMT são sistemas versáteis e altamente eficientes dedicados à resolução deste problema. Eles são amplamente utilizados na indústria para a automação de aplicações de métodos formais em diversos domínios, tais como verificação de programas, verificação de hardware, análise estática, segurança, geração de testes, síntese de programas, dentre outros”, explicou.
De acordo com o professor, o artigo foi fruto de um trabalho de vários anos de um grande número de pesquisadores, da Stanford University e University of Iowa nos EUA, da UFMG, da City, University of London, na Inglaterra, e da Bar-Ilan University, em Israel. “O solucionador cvc5 representa um marco na área de automatização de raciocínio e de resolução do problema SMT, e deve continuar por vários anos sendo relevante na área e em suas aplicações na academia e na indústria. Além disso, o sistema continua sendo ativamente estendido e melhorado e, da mesma forma, usado em vários projetos, inclusive dois deles que coordenam são financiados pela Amazon Web Services”, concluiu.