Banca de DEFESA: VÍTOR ALCÂNTARA DE ALMEIDA

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE: VÍTOR ALCÂNTARA DE ALMEIDA
DATA: 29/04/2016
HORA: 08:30
LOCAL: Auditório do CCET
TÍTULO:

WPTrans: Um Assistente para Verificação de Programas em Frama-C.


PALAVRAS-CHAVES:

Frama-C, WP, WPTrans, Obrigação de Prova, Coq, SMT. 


PÁGINAS: 150
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
ESPECIALIDADE: Linguagens de Programação
RESUMO:

A presente dissertação descreve uma extensão para a plataforma Frama-C e o plugin WP:
o WPTrans. Essa extensão permite a manipulação, através de regras de inferência, das
obrigações de prova geradas pelo WP, com a possibilidade das mesmas serem enviadas,
em qualquer etapa da modificação, a solucionadores SMT e assistentes de prova. Algumas
obrigações de prova podem ser validadas automaticamente, enquanto outras são muito
complexas para os solucionadores SMT, exigindo uma prova manual pelo desenvolvedor,
através dos assistentes de prova. Contudo, a segunda abordagem geralmente requer do
usuário uma experiência significativa em estratégias de prova. Alguns assistentes oferecem
comunicação com provadores automáticos, entretanto, esta ligação pode ser complexa
ou incompleta, restando ao usuário apenas a prova manual. O objetivo deste plugin é interligar
os dois tipos de ferramentas de modo preciso e completo, com uma linguagem
simples para a manipulação. Assim, o usuário pode simplificar suficientemente as obrigações de
prova para que possam ser validadas por qualquer outro solucionador SMT.
Não obstante, a extensão é interligada diretamente ao WP, facilitando a instalação do
plugin no Frama-C. Esta extensão também é uma porta de entrada para outras possíveis
funcionalidades, sendo as mesmas discutidas neste documento.


MEMBROS DA BANCA:
Presidente - 1495704 - UMBERTO SOUZA DA COSTA
Interno - 2220777 - DAVID BORIS PAUL DEHARBE
Externo à Instituição - PLACIDO ANTONIO DE SOUZA NETO - IFRN
Externo à Instituição - RICHARD WALTER ALAIN BONICHON - UPMC
Notícia cadastrada em: 19/04/2016 00:43
SIGAA | Superintendência de Informática - (84) 3215-3148 | Copyright © 2006-2017 - UFRN - sigaa07-producao.info.ufrn.br.sigaa07-producao