Bolsista de pós-graduação – Mestrado e Doutorado – Prof. Haniel Barbosa


O professor Haniel Barbosa está com bolsas disponíveis tanto para alunos de mestrado como de doutorado, para trabalhar na área de métodos formais, especificamente em automatização de raciocínio e resolução SMT (satisfatibilidade módulo teorias).

As inscrições para os programas de mestrado e doutorado em Ciência da Computação na UFMG estão abertas. As inscrições do mestrado vão até 24 de janeiro, com início em 2022. As inscrições para doutorado são em fluxo contínuo. Consulte os editais: https://ppgcc.dcc.ufmg.br/editais

++++ Logística

Aqueles que se interessarem devem entrar em contato comigo pelo e-mail hbarbosa@dcc.ufmg.br.

Os valores das bolsas (negociáveis):
– Mestrando: R$ 2.000,00 (1º ano) e R$ 2.200,00 (2º ano)
– Doutorando: R$ 3.000,00 (1º ano) e R$ 3.700,00 (2º ano em diante)

As atividades poderão ser desenvolvidas remotamente enquanto durarem os protocolos de distanciamento definidos pela administração da UFMG (atualmente planejando volta presencial em abril de 2022).

Será fornecido auxílio instalação/deslocamento para estudantes de fora de Belo Horizonte. Valores poderão ser discutidos quando iniciado o contato.

++++ Tópicos de pesquisa

As atividades de pesquisa deverão ser desenvolvidas no contexto de resolução SMT e automatização de raciocínio. Pesquisas nessa área envolvem tanto teoria como prática, com desenvolvimento de novas técnicas e sua implementação e avaliação. O sistema base será o solucionador SMT cvc5 (https://cvc5.github.io/).

Possíveis tópicos de pesquisa:

– Demonstrações de solucionadores SMT (SMT proofs)

* Verificação e reconstrução de demonstrações (proof checking, proof reconstruction).

* Compressão de demonstrações (proof compression).

* Diagnóstico de que partes de um problema são difíceis para o solucionador SMT.

O foco dos problemas acima é na certificação dos resultados de solucionadores SMT para assistentes de demonstração (como Lean, Coq, Isabelle/HOL) e
ferramentas de verificação formal em geral.

– Raciocínio com quantificadores em SMT (Quantifier reasoning in SMT)

* Aumento da escalabilidade de técnicas de instanciação existentes.
* Quantificadores de ordem superior (higher-order quantifiers).

O foco dos problemas acima é na escalabilidade de solucionadores SMT em geral.

– Síntese de programas baseada em SMT (SMT-based program synthesis)

* Integração de técnicas de aprendizado de máquina para síntese de invariantes (invariant synthesis)
* Escalabilidade de síntese módulo teorias providas por usuários com funções recursivas

O foco desses problemas é no aumento da escalabilidade de síntese de programas baseada em SMT.

++++ Oportunidades

Além da disponibilidade de recursos para participação em eventos (nacionais e internacionais), há ainda a oportunidade de colaboração com outros pesquisadores trabalhando em tópicos similares, tanto na UFMG como nas universidades de Iowa e de Stanford (EUA).

As bolsas desta chamada são financiadas pela Amazon Web Services, uma dentre muitas empresas que vem investindo fortemente em métodos formais e automatização de raciocínio. Elas frequentemente procuram pesquisadores dessas áreas para realização de estágios e o mercado é bastante favorável a profissionais especialistas nessa área.


Início divulgação: 12/01/2022
Data limite para candidatura: 30/04/2022

Coordenador do projeto: - Haniel Moreira Barbosa

Tipo: Bolsa

Situação: Ativo


Email para candidatura: hbarbosa@dcc.ufmg.br