A bolsa é destinada para a pesquisa e instrumentalização de uma técnica de conversão conhecida entre problemas com vetores de bits para pseudo-booleanos. Grande parte do trabalho prático será realizado no solucionador SMT cvc5 (https://cvc5.github.io/). O principal objetivo é avaliar comparativamente a resolução e produção de certificados de insatisfatibilidade desses novos problemas em relação ao estado da arte.

A bolsa é no contexto do projeto “PEGISUS: Proof EnGineering and Integration with Satisfiability modUlo theorieS”, financiado pela Defense Advanced Research Projects Agency (DARPA), e a IC é com orientação do professor Haniel Barbosa (https://hanielbarbosa.com/).

Valor: R$1350,00/mês

Período para se candidatar: até 27/03/2026
Início previsto: Abril/2026

Duração: 1 ano (com possibilidade de renovação dependendo do interesse mútuo)

Requisitos:
– saber programação em C++ (desejável ter o quarto período do curso integralizado),
– não ter vínculo empregatício,
– ter disponibilidade de 20 horas semanais,
– bom conhecimento de lógica computacional é desejável mas não obrigatório.

Vantagens e oportunidades:
– possibilidade de publicação de artigos científicos,
– contato com pesquisadores internacionais (Stanford, Iowa, Copenhagen).

++++++

Interessados devem enviar um email para hbarbosa@dcc.ufmg.br com seu histórico e um mini-currículo.