DCC/UFMG

Solucionadores SMT são amplamente utilizados na indústria para a automação de aplicações de métodos formais em diversos domínios, tais como verificação de programas, verificação de hardware, análise estática, segurança, geração de testes, síntese de programas, etc. Veremos como utilizar solucionadores SMT para resolver diversos problemas computacionais que surgem nesses domínios.

Esta miniapresentação divulgará a iniciativa da Sociedade Brasilieira de Computação (SBC) através da sua Diretoria de Educação em propor um referencial de formação para os cursos de graduação em Bacharelado em Cibersergurança. Há uma carência mundial de profissionais nesta área. O objetivo é apresentar de modo simples os eixos que abragerão o curso e sua diferença para os cursos, bem como tirar dúvidas da audiência desde o contéudo técnico até as possíveis áreas de atuação.

Muitos jogos e quebra-cabeças atraem o interesse de pessoas em busca de desafios intelectuais. De certa forma, a dificuldade de uma atividade ajuda a torná-la instigante: um quebra-cabeça muito simples rapidamente se torna desinteressante. Frequentemente tal dificuldade pode ser formalizada, permitindo demonstrar que tais jogos também são difíceis, em diferentes níveis, até mesmo para modelos computacionais.

O estudo da dificuldade de jogos acompanhou os avanços da complexidade computacional, não só utilizando as ferramentas já existentes para a determinação da dificuldade de certos jogos, mas também motivando o desenvolvimento e formalização de novas ideias e modelos.

Nesta palestra discute-se como diferentes jogos (ou mesmo diferentes versões de um mesmo jogo) se posicionam em diversas classes de complexidade, não só nas famosas classes P e NP, mas até em classes mais gerais, como PSPACE e EXP.

Apesar do entusiasmo atual associado ao uso de algoritmos de mineração de dados e aprendizado de máquina, seu uso real ainda é um desafio em vários cenários de aplicação e há uma consciência crescente da necessidade desses algoritmos serem compatíveis com valores éticos, morais e humanos. Nesta palestra, argumentamos que empregar esses modelos e técnicas efetivamente exige que eles sejam contextualizados ao domínio, interpretáveis para os usuários finais e automatizados tanto quanto possível. Discutiremos esses requisitos e apresentaremos alguns resultados recentes que alcançamos no âmbito das aplicações em saúde, em particular na cardiologia.

LLVM é um conjunto de bibliotecas e ferramentas que facilitam o desenvolvimento de linguagens de programação. Várias linguagens populares hoje são construídas e compiladas via LLVM: C, C++, Rust e Julia, por exemplo. LLVM define uma representação intermediária de código (uma linguagem de montagem). Ao traduzir uma linguagem de alto nível para este código intermediário, tem-se acesso a uma vasta gama de análises estáticas e otimizações que já estão disponíveis em LLVM. Nessa palestra veremos como usar LLVM como uma ferramenta para compilar e visualizar programas, escreveremos código na representação intermediária, e desenvolveremos uma análise de código que pode ser acoplada àquela infra-estrutura.

O debate político e a disputa eleitoral no espaço online durante as eleições brasileiras de 2018 marcaram o início de uma grande guerra informacional no país. Essa guerra se tornou parte do nosso cotidiano e um dos problemas mais desafiadores da nossa sociedade. Visando mitigar o problema, nós criamos o projeto “Eleições Sem Fake” (www.eleicoes-sem-fake.dcc.ufmg.br) e desenvolvemos soluções tecnológicas capazes de monitorar e expor as atuações de diferentes campanhas políticas no espaço online. Exemplos de sistemas incluem: um monitor de propagandas impulsionadas no Facebook e monitores de grupos públicos, voltados para discussão política, no WhatsApp e no Telegram. Nossos sistemas se mostraram fundamentais para a checagem de fatos, para o jornalismo investigativo e, atualmente, nosso projeto faz parte da frente nacional de enfrentamento à desinformação do TSE. Essa palestra sumariza uma série de lições aprendidas a partir da implantação desses sistemas e aponta direções futuras para o combate à desinformação.

Apesar de vários esforços para detecção e combate à desinformação online, as campanhas de fake news, em particular em plataformas de mídia social, permanecem um problema com grande impacto nas sociedades. Nós argumentamos que para desenvolver soluções efetivas para o combate à desinformação é essencial entender (analisar e modelar) como a informação é propagada, frequentemente cruzando os limites de diferentes plataformas, e atingindo uma grande audiência. Nesta palestra, eu irei discutir alguns dos desafios principais para o combate à desinformação online a apresentar resultados recentes do nosso grupo de pesquisa sobre a análise de disseminação de fake news. Nossos resultados abordam aspectos relacionados ao conteúdo, dinâmica de propagação e à rede de disseminação de informação, bem como características dos usuários, enquanto seres humanos, que mais contribuem para o espalhamento de desinformação na Web.