A bolsa é destinada para a pesquisa e instrumentalização de técnicas combinando satisfatibilidade módulo teorias (SMT) e programação linear/não-linear/inteira. A bolsa envolve trabalho prático principalmente no solucionador SMT cvc5 (https://cvc5.github.io/) e na sua integração com o SCIP (https://www.scipopt.org/). O principal objetivo é avaliar o impacto do uso do SCIP no cvc5 e explorar a produção de certificados para raciocínio em aritmética não-linear via somas de quadrados, calculadas através de programação semidefinida.

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/) e do professor Marcio Santos (/professor/marcio-costa-santos/).

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++
– ter cursado ou estar cursando a disciplina de Pesquisa Operacional
– 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 e contato com pesquisadores internacionais (Stanford, Iowa).

++++++

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