Alice/my_digital_garden
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
my_digital_garden/4a1s/MFES/MFES - UC Details.md

1.7 KiB
Raw Blame History

dg-publish
true

🌫 11 Setembro 2023 - #MFES

Programa

  1. Lógicas para especificação formal
    1. MFES/T - Aula 2#Proposicional Logic (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

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.