WPTrans: um assistente para verifica??o de programas em Frama-C

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-08-26T23:09:02Z No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5)

Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-08-30T23:32:12Z (GMT) No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5)

Made available in DSpace on 2016-08-30T23:32:12Z (GMT). No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5) Previous issue date: 2016-04-29

Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior (CAPES)

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.

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.