Verificação de Programas

Código:

CC4085

Sigla:

CC4085

Nível:

400

Áreas Científicas
Classificação	Área Científica
OFICIAL	Ciência de Computadores

Ocorrência: 2022/2023 - 2S

Ativa?	Sim
Página Web:	https://www.dcc.fc.up.pt/~nam/Teaching/vp23/index.php
Unidade Responsável:	Departamento de Ciência de Computadores
Curso/CE Responsável:	Mestrado em Ciência de Computadores

Ciclos de Estudo/Cursos

Sigla	Nº de Estudantes	Plano de Estudos	Anos Curriculares	Créditos UCN	Créditos ECTS	Horas de Contacto	Horas Totais
M:CC	5	PE a partir do ano letivo de 2014	1	-	6	42	162

Língua de trabalho

Português - Suitable for English-speaking students

Objetivos

No desenvolvimento de sistemas informáticos de software ou hardware é essencial garantir a sua correção em relação à especificação inicial. No ciclo de produção, o tempo gasto em verificação tem levado a indústria a procurar a utilização de métodos formais de verificação em detrimento de métodos ad-hoc baseados em testes/simulação, que dificilmente cobrem todos os casos e não permitem garantir de forma rigorosa a fiabilidade e segurança dos sistemas. A verificação, sendo um imperativo na área dos sistemas críticos e de tempo real, tem vindo a ser estendida a outras áreas dos sistemas informáticos (p.e. ao comércio eletrónico). Neste contexto, a unidade curricular de Verificação de Programas tem como objetivo a introdução a técnicas formais de verificação de sistemas informático em sistemas dedutivos. 

Resultados de aprendizagem e competências

Pretende-se que o aluno:

 

• perceba a importância da utilização da lógica e dos sistemas formais no desenvolvimento de sistemas informáticos complexos;
• seja capaz de anotar programas simples duma linguagem imperativa ou orientada a objetos de modo a garantir propriedades de segurança e propriedades funcionais; e de especificar teorias que permitam a modelação de estruturas mais complexas, cuja correção será demonstrada por um demonstrador automático ou interativo;
• adquira conceitos básicos de demonstradores automáticos de teorias lógicas decidíreis (SMT-provers) e demonstradores interactivos
• adquira os princípios básicos de modo a permitir-lhe a utilização das ferramentas adequadas de verificação (formal) na sua vida profissional futura ou o desenvolvimento de trabalhos de investigação na área de métodos formais;

Modo de trabalho

Presencial

Pré-requisitos (conhecimentos prévios) e co-requisitos (conhecimentos simultâneos)

Conhecimentos de lógica proposicional e de primeira ordem. Noções de básicas  semanticas  operacionais e algoritmos e estruturas de dados..

Programa

 

1. Breve introdução aos métodos formais e a técnicas de verificação formal.
2. Verificação de Dedutiva de Programas
   
   • Cálculos de correção parcial e total (Lógicas de Hoare).
   • ◦Pré-condições mais fracas e algoritmos de geração de condições de verificação.
   • ◦Verificação de segurança e verificação funcional.
   • ◦Ferramentas para a especificação, verificação e certificação de programas imperativos: geradores de condições de verificação.
   • ◦Correção de programas simples sobre inteiros e estruturas de dados usuais
3. Demonstração Automática e Interactiva

• Lógica proposicional: SAT solvers.

• Teorias decidíveis: inteiros, reais, arrays, apontadores, etc.

• SMT solvers: algoritmos de decisão e sua combinação

• Utilização de uma ferramenta de demonstração automática (p.e Z3)

• Breve introdução aos tipos dependentes e ao demonstrador interactivo Coq (ou semelhante)

 

 

 

 

Bibliografia Obrigatória

Almeida José Bacelar 070; Rigorous software development. ISBN: 9780857290175
Daniel Kroening; Decision procedures. ISBN: 978-3-540-74104-6

Bibliografia Complementar

Huth Michael 1962-; Logic in Computer Science. ISBN: 0-521-54310-X
Yves Bertot; Interactive theorem proving and program development. ISBN: 9783540208549 hbk
Benjamim Pierce et al.; Software Foundations (https://softwarefoundations.cis.upenn.edu)

Métodos de ensino e atividades de aprendizagem

Aulas expositivas e resolução de problemas e casos de estudo.

Software

LEAN
Z3
Dafny
Coq

Tipo de avaliação

Avaliação distribuída com exame final

Componentes de Avaliação

Designação	Peso (%)
Exame	40,00
Trabalho escrito	30,00
Trabalho prático ou de projeto	30,00
Total:	100,00

Componentes de Ocupação

Designação	Tempo (Horas)
Estudo autónomo	80,00
Frequência das aulas	42,00
Trabalho escrito	40,00
Total:	162,00

Obtenção de frequência

Frequência a 3/4 das aulas teórico práticas

Fórmula de cálculo da classificação final

Serão propostos trabalhos práticos durante o semestre. A classificação final é calculada como média aritmética
das classificações dos trabalhos práticos (TP) e do exame (E)  com os seguintes pesos: 0.6*TP+0.4*E.
A nota mínima do exame (E)  é 6 em 20 e cada trabalho prático proposto tem de ter nota mínima de 5 em 20.

Nota mínima total: 9.5 em 20

Avaliação especial (TE, DA, ...)

Não há avaliação especial

Melhoria de classificação

O exame de melhoria de classificação é para 20 valores

Observações

.