8ª Aula

10 Abril 2017, 14:00 • João Marques Silva

A oitava aula iniciou o estudo de Satisfação Módulo Teorias (Satisfiability Modulo Theories, SMT). Foram apresentados exemplos de motivação incluindo os problemas de cooperative pathfinding, job-shop scheduling, e symbolic execution. A aula apresentou uma perspectiva de teorias de primeira ordem de interesse, incluindo igualdade com funções não interpretadas, aritmética linear e não linear, lógica de diferenças, bit vectors, entre outros. A aula descreveu também os algoritmos utilizados para resolver fórmulas SMT, os quais incluem as abordagens Eager e Lazy. A aula incluiu uma demonstração do resolvedor SMT Z3, e também da sua interface Python.