Temos duas bolsas de pós-doutorado no DCC/UFMG para o grupo de pesquisa SMITE, que trabalha com técnicas baseadas em SMT para aumentar a escalabilidade e confiança de aplicações de métodos formais. Os bolsistas contribuirão para o projeto, financiado pela DARPA, PEGISUS: Proof EnGineering and Integration with Satisfiability modUlo theorieS.

As atividades serão: implementar técnicas eficientes de verificação de demonstrações em um novo formato baseado em SMT-LIB 3, melhorar a busca e produção de demonstrações no solucionador SMT cvc5, e habilitar a conexão entre solucionadores SMT e assistentes de demonstração.

É necessário ter doutorado em Ciência da Computação ou algum campo próximo, com uma boa formação em automatização de raciocínio, métodos formais ou lógica.

Candidato(a) ideal:

– Conhecimento e experiência com C++, Rust, ou Lean – Inglês avançado para escrita e conversação – Capacidade de trabalhar em um ambiente colaborativo – Forte compromisso com a excelência em pesquisa

Carga horária e local de trabalho: 40h/semana para trabalhar em Belo Horizonte, Brasil.

A bolsa, sem impostos, é de R$10.000,00, bem como financiamento para viagens a trabalho e para cobrir despesas de instalação para candidatos fora de Belo Horizonte, que pode ser estendida baseado em desempenho e disponibilidade de recursos.

As vagas ficarão abertas até serem preenchidas.

Data de início: Imediato

Candidatura: Enviar e-mail para Haniel Barbosa (hbarbosa@dcc.ufmg.br) com seu CV (incluindo uma lista de publicações), uma carta curta explicando o motivo de se encaixar na vaga, e nomes de ao menos duas referências. A seleção será baseada em currículo e entrevistas (on-line) para candidatos pré-selecionados.

Colaborações: Os candidatos selecionados terão a oportunidade de colaborar ativamente com a Stanford University, a University of Iowa e a Bar-Ilan University, no contexto do projeto PEGISUS e em tópicos relacionados.