---
dg-publish: true
---
🌫 11 Setembro 2023 - #MFES

## Programa

1. Lógicas para especificação formal
	1. [[MFES/T - Aula 2#Proposicional Logic (PL)| Lógica Proposicional (PL)]]
	2. Lógica de Primeira Ordem (FOL)
	3. Lógica relacional (RL)
	4. Lógica temporal linear (LTL)
2. Técnicas de prova automática
	1. SAT solving para lógica proposicional
	2. SMT solving para lógica e teorias de primeira ordem
	3. Model-finding via SAT para lógica relacional
	4. Bounded model-checking via SAT para lógica temporal
3. Concepção formal de software com Alloy
	1. Modelação estrutural
	2. Modelação comportamental
4. Especificação e verificação de programas com Why3
	1. Linguagem lógica, teorias (biblioteca) e prova
	2. Linguagem de programas, especificação comportamental, e verificação de correção
	3. Desenvolvimento de sistemas com estado
  
## Docentes
- Maria João Frade - [mjf@di.uminho.pt](mailto:mjf@di.uminho.pt)
- Alcino Cunha - [alcino@di.uminho.pt](mailto:alcino@di.uminho.pt)
- Jorge Sousa Pinto - [jsp@di.uminho.pt](mailto:jsp@di.uminho.pt)
  
## Avaliação
- 20% - Exercícios de avaliação
- 80% - Teste individual   

Nota: As notas acima de 18 valores (quer na avaliação contínua quer no exame) terão que ser defendidas através da realização de um pequeno projecto.

  
## Planificação
- 6 Outubro - Entrega do 1º exercício de avaliação. Modelação em PL e FOL.
- 27 Outubro - Entrega do 2º exercício de avaliação. Modelação estrutural em Alloy.
- 10 Novembro - Entrega do 3º exercício de avaliação. Modelação comportamental em Alloy.
- 8 Dezembro - Entrega do 1º exercício de avaliação. Desenvolvimento e verificação de sistemas com estado em Why3.