Verificação de Programas

A aula de hoje foi minha última aula de Lógica para Computação no 1o. semestre (letivo) de 2012. Foi sobre Verificação de Programas. Os slides usados estão abaixo:

Especificação e Verificação de Programas from Adolfo Neto


 

Verificação de Programas from Adolfo Neto


Além de apresentar os slides, gosto de, durante a aula, mostrar páginas relacionadas ao tema, para ilustrar o assunto.

Alguns dos links foram:

• O que é especificação? por C.A.R. Hoare, em que ele diz que "Uma especificação é apenas um teste generalizado".    Tony Hoare, para quem não sabe, é um dos vencedores do Prêmio Turing. Um Cientista da computação com grandes contribuições.
• Gerard Holzmann é um holandês, criador do SPIN model checker, que atualmente trabalha no JPL da Nasa, um dos principais centros de pesquisa em verificação formal no mundo.
• A página sobre Métodos Formais na Wikipédia lista várias das notações e métodos existentes para fazer especificação e verificação formal.
• Como falo que grandes empresas de desenvolvimento de chips usam verificação formal, encontrei este link da Verificação Formal de um chip ARM.
• O software dos bafômetros dá problema!
• Software dá problema pois temos que escrever na linguagem que o computador entende. Que linguagem é essa? Você pode ter uma ideia lendo este texto sobre a atividade Computador a Papel.
• Não existe computador inteligente! Não existe sistema inteligente!
• Vídeo da visita da turma do PhD Comics ao JPL da Nasa: