Quartz sync: Sep 19, 2023, 7:39 PM

content/MFES/MFES - UC Details.md

@@ -1,37 +0,0 @@
-## Programa
-
-1. Lógicas para especificação formal
-	1. [[T - Aula 2 - 18 Setembro 2023#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.