Use este identificador para citar ou linkar para este item: https://repositorio.ufrn.br/jspui/handle/123456789/21290
Título: WPTrans: um assistente para verificação de programas em Frama-C
Título(s) alternativo(s): WPTrans: a proof assistant for program verification in Frama-C
Autor(es): Almeida, Vítor Alcântara de
Palavras-chave: Frama-C;WP;WPTrans;Obrigação de prova;Coq;SMT
Data do documento: 29-Abr-2016
Editor: Universidade Federal do Rio Grande do Norte
Citação: ALMEIDA, Vítor Alcântara de. WPTrans: um assistente para verificação de programas em Frama-C. 2016. 150f. Dissertação (Mestrado em Sistemas e Computação) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2016.
Resumo: The platform Frama-C is a tool dedicated to analysis of source code of software written in C, with the possible types of analysis provided by plugins attached to the platform. One of its plugins is WP, used for deductive veri cation of C code with ACSL, a formal speci cation language. This dissertation describes the extension of this plugin, named WPTrans. This extension allows generated proof obligations from WP to be manipulated through inference rules and sent, at any stage of the proof, to automatic (mainly SMT solvers) and interactive theorem provers. Some proof obligations may be proved automatically, while others can be too complex to be solved by automatic theorem provers, requiring the users of Frama-C and WP to handle them manually. This approach usually requires a signi cant experience in proof strategies. Some interactive theorem provers provide communication with automatic provers. However, this connection can be complex and incomplete, leaving the user with the manual proof option only. The strength of WPTrans is to combine the features of automatic and interactive theorem provers in a precise and complete way, with a simple manipulation language. Thus, the user can simplify the proof obligations enough in order for its proof to be concluded with an SMT solver, letting the proof be partially manual and partially automatic. Nevertheless, the plugin is directly linked do WP, facilitating the installation of the extension in Frama-C. This tool is also a gateway to other possible features, which we discuss herein.
metadata.dc.description.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, dasobrigaçõ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. Algumasobrigações de prova podem ser validadas automaticamente, enquanto outras são muitocomplexas para os solucionadores SMT, exigindo uma prova manual pelo desenvolvedor,através dos assistentes de prova. Contudo, a segunda abordagem geralmente requer dousuário uma experiência significativa em estratégias de prova. Alguns assistentes oferecemcomunicação com provadores automáticos, entretanto, esta ligação pode ser complexaou incompleta, restando ao usuário apenas a prova manual. O objetivo deste plugin é interligaros dois tipos de ferramentas de modo preciso e completo, com uma linguagemsimples para a manipulação. Assim, o usuário pode simplificar suficientemente as obrigações deprova para que possam ser validadas por qualquer outro solucionador SMT.Não obstante, a extensão é interligada diretamente ao WP, facilitando a instalação doplugin no Frama-C. Esta extensão também é uma porta de entrada para outras possíveisfuncionalidades, sendo as mesmas discutidas neste documento.
URI: http://repositorio.ufrn.br/handle/123456789/21290
Aparece nas coleções:PPGSC - Mestrado em Sistemas e Computação

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
VitorAlcantaraDeAlmeida_DISSERT.pdf2,19 MBAdobe PDFThumbnail
Visualizar/Abrir


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.