Olá, Estão abertas inscrições para os programas de mestrado e doutorado em Ciência da Computação na UFMG. As inscrições do mestrado vão até 24 de janeiro, com início em abril de 2022. As inscrições para doutorado são em fluxo contínuo. O edital se encontra aqui: https://ppgcc.dcc.ufmg.br/wp-content/uploads/2021/12/Edital-Regular-de-Selecao-PPGCC-2022-13dezembro2021.pdf
Eu tenho bolsas disponíveis tanto para estudantes 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). ++++ Logística Aqueles que se interessarem devem entrar em contato comigo pelo e-mail hbarb...@dcc.ufmg.br. Os valores das bolsas (negociáveis): - Mestrando: R$ 2.000,00 (1o ano) e R$ 2.200,00 (2o ano) - Doutorando: R$ 3.000,00 (1o ano) e R$ 3.700,00 (2o 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. Se puderem encaminhar para possíveis interessados agradeço muito. Abraço, -- Haniel Barbosa https://homepages.dcc.ufmg.br/~hbarbosa/ -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para logica-l+unsubscr...@dimap.ufrn.br. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/87bl0hsyvm.fsf%40gmail.com.
