Objetivos | A UC é estrutural porque fornece a experiência, em ferramentas conceptuais e computacionais, necessárias à especificação e verificação automática de grandes sistemas definidos por regras lógicas complexas.
Pretende-se atingir familiaridade com um conjunto de problemas lógicos "standard" aos quais muitos sistemas concretos podem ser reduzidos e fornecer proficiência com as ferramentas computacionais usadas na construção das suas soluções. |
Programa | 1. Optimização. Problemas de "programação inteira" (IP), "programação inteira híbrida" (MIP) e "programação com restrições" (CP). Algoritmos de otimização em MIP e CP. Problemas Knapsack, Set Cover, Point Cover. Alguns problemas de Grafos.
2. Satisfação Proposicional (SAT). Algoritmo de Davis Putman e suas oprimizações. Problemas MAXSAT.
3. "Satisfiability Model Theories" (SMT). Algoritmos base de verificação SMT. As principais teorias SMT. Verificação da correcção de programas imperativos. Sistemas de Transição de 1ª Ordem (FOTS) e sua codificação em SMT's. Sistemas ciber-físicos (autómatos híbridos) e a sua codificação em SMT's.
4. Verificação de Modelos Finitos ("Model Checking"). Lógicas temporais LTL e CTL. Estruturas de Kripke. BDD's ("binary decision diagrams") e os seus algoritmos. "Model Checking" usando BDD's.
5. "Bounded Model Checking" (BMC). Verificação de modelos infinitos. Descrição do comportamento limitado de sistemas infinitos. Codificação da LTL e verificação de fórmulas LTL num comportamento infinito usando SMT's. |
Bibliografia | Integer Programming, Conforti, Michele, Cornuejols, Gerard, Zambelli, Giacomo, Springer-Verlag.
Biere, A. (ed). Handbook of Satisfiability. IOS Press.
Manuais dos sistemas SCIP, Gurobi, MiniSat, Z3, SMTLIB, NuSMV, XuSMV. |
Resultados da aprendizagem | - Desenvolver conhecimento na modelação lógica de sistemas dinâmicos e das suas propriedades.
- Desenvolver conhecimento na modelação de propriedades de sistemas estáticos e construção de soluções ótimas para a verificação dessas propriedades.
- Desenvolver conhecimento sobre o processo interno de construção de soluções para os problemas de verificação quer de sistemas estáticos como de sistemas dinâmicos.
- Demonstrar capacidade de usar as ferramentas computacionais mais apropriadas à representação dos sistemas dinâmicos e verificação automática das suas propriedades comportamentais.
- Demonstrar capacidade de adequar as ferramentas computacionais a cada sistema concreto e combinar várias ferramentas quando uma só não basta para resolver o problema.
- Demonstrar capacidade para a construção de algoritmos e flexibilidade para os programar nas linguagens que forem necessárias.
Pré-requisitos recomendados
Noções elementares de Matemática Discreta e Lógica. |
Departamento de Informática (UM)