Exercícios de Verificação Formal de Software
Model Checking
- Sistemas de Transição e Comunicação entre Processos
- Propriedades Temporais Lineares
- Lógica LTL
- Lógica CTL
- Algoritmo de model checking para CTL
- OBDDs e model checking simbólico de CTL
- Autómato de Buchi Alternados e Algoritmo de Model checking para LTL
- Cálculos de correção parcial e total Regras da Lógica de Hoare