Lógica e Verificação de Modelos

O objetivo da cadeira é aprender algoritmos de model checking, i.e., algoritmos que provam ou refutam propriedades sobre programas imperativos. O caminho que se faz para alcançar este objetivo é a parte interessante: aprendemos duas lógicas modais (temporal linear e branching), aprendemos sobre como vários tipos de autómatos (determinísticos, buchi, etc) servem para estudar linguagens e como fórmulas de lógica temporal podem ser transformadas nestes autómatos, e aprendemos a utilizar ferramentas como o algoritmo SAT (implementado pelo Z3) e a linguagem Spin.

A avaliação em exame + 2 projetos...