Banca de QUALIFICAÇÃO: VÍTOR ALCÂNTARA DE ALMEIDA

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE: VÍTOR ALCÂNTARA DE ALMEIDA
DATA: 27/11/2015
HORA: 10:00
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: 87
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:

Esta dissertação descreve a fase inicial de um plugin para Frama-C e WP: o WPTrans. Ela é uma extensão que permite a manipulação, através de regras de inferência, das obrigações de prova geradas pelo WP, com a possibilidade de envio, em qualquer etapa da modi cação, a solucionadores SMT e outros provadores de teoremas. Algumas obrigações de prova podem ser validadas automaticamente, enquanto outras são muito complexas para os so- lucionadores SMT, exigindo uma prova manual pelo desenvolvedor, através dos assistentes de prova: esta abordagem geralmente requer do usuário uma experiência signi cativa 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 simpli car su cientemente as obrigações de prova para que possam ser validadas por qualquer outro solucionador SMT. Não obstante, a ferramenta é interligada diretamente ao WP, facilitando a instalação do plugin no Frama-C. Esta ferramenta também é uma porta de entrada para outras possíveis funcionalidades, sendo as mesmas discutidas neste documento. 


MEMBROS DA BANCA:
Presidente - 2220777 - DAVID BORIS PAUL DEHARBE
Interno - 1495704 - UMBERTO SOUZA DA COSTA
Externo ao Programa - 1845280 - SERGIO QUEIROZ DE MEDEIROS
Externo à Instituição - RICHARD WALTER ALAIN BONICHON - UPMC
Notícia cadastrada em: 19/11/2015 16:50
SIGAA | Superintendência de Informática - (84) 3215-3148 | Copyright © 2006-2017 - UFRN - sigaa05-producao.info.ufrn.br.sigaa05-producao