Programa

Software Fiável

Mestrado Bolonha em Engenharia Informática

Mestrado Bolonha em Informática

Mestrado Bolonha em Segurança Informática

Programa

Visão geral dos métodos de fiabilidade de software e verificação formal. Verificação dedutiva de programas e o Cálculo de Hoare. Design por contrato para abstrações procedimentais e abstrações de dados. A linguagem de programação Dafny e o seu verificador e assistente de provas automáticas. Os princípios fundamentais do model checking. A lógica temporal linear. A ferramenta de verificação de modelos SPIN. A IA generativa e verificação formal: geração, verificação e ciclos de feedback. Aplicações das ferramentas e técnicas estudadas e uma visão geral de outras técnicas e ferramentas relacionadas.