MFES - UC Details

🌫 11 Setembro 2023 - #MFES

Programa

  1. Lógicas para especificação formal
    1. 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

Avaliação

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