* Verificação Dedutiva de Programas - 2016-1 - Seg/Qua 16-18h *

(Favor divulgar entre os alunos da Engenharia de Computação, Matemática e Matemática Industrial.)

* RESUMO: Nesta disciplina aprendemos a demonstrar matematicamente a corretude de algoritmos e programas estruturados. Na prática, isso é feito anotando-se suficientemente o código-fonte com (a) asserções que especificam relações matemáticas entre valores de variáveis, (b) condições exigidas para a execução de certos trechos de código, (c) medidas de terminação, etc (são as pré-/pós-condições, invariantes, variantes, etc). Do ponto de vista teórico, a corretude de tais asserções pode então ser avaliada segundo algum formalismo subjacente (Lógica de Hoare, Weakest Preconditions, Lógica de Separação, etc). Na prática, porém, sabe-se que a "verificação de papel-e-caneta" geralmente não é confiável e muito menos tem a escalabilidade necessária para software real. Por isso, ferramentas computacionais são utilizadas na prática para processar a maior parte dos detalhes triviais, idealmente deixando apenas o trabalho intelectualmente significativo para o verificador humano. Em caso de sucesso, o código-fonte é verificado correto antes mesmo de ser compilado. No geral, o processo de verificação pode produzir fortes garantias sobre um programa, mas por outro lado exige conhecimento matemático preciso da lógica do programa, e por vezes um trabalhoso diálogo entre humano e máquina. O propósito desta disciplina é apresentar os fundamentos dessa atividade e permitir ao aluno a prática do processo, fazendo uso das ferramentas à disposição (Frama-C, Dafny, VeriFast, etc).

* PRÉ-REQUISITOS: para alunos da Ciência da Computação, Estruturas de Dados e Lógica. Para alunos dos demais cursos, Estruturas de Dados e Matemática Discreta (ou equivalentes). Na prática, o necessário é ter desenvoltura com programação e alguma maturidade matemática (raciocínio dedutivo).

* MATRÍCULA: Os alunos que desejarem cursar a disciplina deverão se matricular na turma

  CK0240 - Verificação Dedutiva de Programas - T01 ,

que pertence ao novo currículo de Ciência da Computação (código 95). Os alunos do antigo currículo de Computação (código 65) que não tenham mais créditos "livres" à disposição deverão se matricular na turma

  CK0131 - Tópicos Especiais em Lógica Matemática - T01 ,

que foi criada para atender esse caso específico.
 
* MAIS INFORMAÇÕES: na página da disciplina (em construção) estão a regulamentação oficial da disciplina (com ementa, objetivos, justificativa, bibliografia) e outras informações:

  http://lia.ufc.br/~pmsf/2016-1/vdp/regulamentacao.pdf ,
  http://lia.ufc.br/~pmsf/2016-1/vdp/ .