Departamento de Informática (UM)

Verificação Formal

11602 [MC25MC2503005186]

Mestrado em Matemática e Computação [MMC]

S2

Manuel Alcino Pereira Cunha

Objetivos

O objetivo desta UC é constituir uma introdução geral às áreas de lógica computacional e verificação formal de software. Os objetivos de aprendizagem praticamente não contêm dependências entre si, pelo que são abordados cada um num capítulo do programa (com a exceção do 4º. e 5º. objetivos, que são tratados num mesmo capítulo) numa sequência coerente. O programa desenhado introduz em cada capítulo conceitos fundamentais para um objetivo de aprendizagem e ilustra-os através de pelo menos uma ferramenta de grande popularidade.

Programa

1. Satisfazibilidade lógica e teorias de primeira ordem. Utilização de SAT solvers e de SMT solvers.
2. Verificação Dedutiva: lógicas de programas; geração de condições de verificação; linguagens de especificação comportamental de interfaces de código e design by contract. Utilização de ferramentas de verificação dedutiva.
3. Análise e verificação automática de programas: bounded model checking de código; interpretação abstrata; refinamento de abstrações com base em contraexemplos (CEGAR).
4. Demonstração de Teoremas: introdução à construção interativa de provas com Coq.

Bibliografia

1. Michael Huth and Mark Ryan. 2004. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, New York, NY, USA.
2. Biere, A., Heule, M., Van Maaren, H., Walsh, T. 2009. Handbook of Satisfiability. IOS Press.
3. José Bacelar Almeida, Maria João Frade, Jorge Sousa Pinto, and Simão Melo de Sousa. 2011. Rigorous Software Development: An Introduction to Program Verification (1st ed.). Springer Publishing Company, Incorporated.
4. Aaron R. Bradley and Zohar Manna. 2010. The Calculus of Computation: Decision Procedures with Applications to Verification (1st ed.). Springer Publishing Company, Incorporated.
5. Benjamin Pierce et al. 2007 (with regular updates). Software Foundations series. Volume I: Logical Foundations. (https://softwarefoundations.cis.upenn.edu)

Resultados da aprendizagem

Esta unidade curricular constitui uma introdução aos conceitos de base lógica, fundamentos semânticos da programação, e técnicas utilizados em verificação de software, bem como a diferentes classes de ferramentas utilizadas para prova de primeira ordem, automática e assistida, e para verificação, com diferentes graus de automação, de propriedades de programas.
Assim, no final, os alunos serão capazes de:
• Utilizar ferramentas lógicas com base em satisfazibilidade e teorias de primeira ordem.
• Utilizar ferramentas lógicas de prova assistida, em particular na formalização de propriedades de programas.
• Especificar o comportamento de programas através de contratos e asserções.
• Utilizar ferramentas de verificação dedutiva de programas.
• Explicar o funcionamento das técnicas mais importantes em verificação automática de software.

Método de avaliação

A avaliação é feita através de dois testes, um intercalar e outro final, ambos com peso de 50%, ou alternativamente através de um teste (60%) e um miniprojecto de verificação, (40%).

Funcionamento

Turno: T 1; Docente: Maria João Gomes Frade; Dep.: DI; Horas: 0.
Turno: T 1; Docente: Manuel Alcino Pereira Cunha; Dep.: DI; Horas: 0.
Turno: T 1; Docente: Jorge Miguel Matos Sousa Pinto; Dep.: DI; Horas: 0.
Turno: TP 1; Docente: Maria João Gomes Frade; Dep.: DI; Horas: 0.
Turno: TP 1; Docente: Manuel Alcino Pereira Cunha; Dep.: DI; Horas: 0.
Turno: TP 1; Docente: Jorge Miguel Matos Sousa Pinto; Dep.: DI; Horas: 0.