Os RSS Meetups são encontros mensais dos membros do LASIGE com interesses de investigação principalmente em Arquitetura de Software, Verificação, Testes, Linguagens de Programação, Sistemas de Tipos, Lógica, Concorrência e Métodos Formais.
Speaker: Tiago Ferreira (UCL)
Tiago Ferreira é aluno do último ano do doutorado no grupo de Princípios de Programação, Lógica e Verificação (PPLV) da University College London, orientado pelos professores Alexandra Silva e Peter O'Hearn. É licenciado em Computação Matemática pela UCL e já estagiou na Galois. A sua investigação centra-se na aprendizagem de autômatos para métodos formais leves, com o objetivo de tornar essas técnicas práticas e acessíveis a não especialistas e indústrias em rápida evolução.
O software moderno depende cada vez mais do comportamento correto das redes de computadores e dos seus protocolos subjacentes. No entanto, esses sistemas são frequentemente desenvolvidos e implementados sem modelos ou especificações formais, dificultando a sua análise e verificação.
A aprendizagem de autômatos é uma abordagem baseada em princípios para recuperar automaticamente modelos formais de sistemas opacos, com garantias de correção. Ao interagir sistematicamente com sistemas fechados, como componentes de rede ou implementações de protocolos, podemos inferir modelos precisos do seu comportamento em vários níveis de abstração, desde servidores individuais até redes inteiras.
Nesta palestra, veremos como a teoria dos autômatos fornece as bases sólidas de correção que tornam a aprendizagem de autômatos rigorosa e prática. Discutirei como esses algoritmos alimentam o PROGNOSIS, uma ferramenta usada para habilitar técnicas de verificação poderosas, como verificação de modelos e detecção automatizada de bugs, que expôs problemas que vão desde vulnerabilidades DoS em software implantado globalmente até falhas de design em protocolos de rede modernos.
Se o tempo permitir, também abordarei como as técnicas simbólicas permitem um novo algoritmo para a aprendizagem de programas NetKAT, uma DSL para verificação de rede, e como os métodos de aprendizagem automática podem melhorar a usabilidade da aprendizagem de autômatos em domínios complexos sem comprometer as suas garantias formais.
Todos são bem-vindos, incluindo estudantes e não investigadores.
Vem participar no dia 17 dezembro, às 10h30, na sala 6.2.47 na CIÊNCIAS ULisboa