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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/21290 |
| Date | 29 April 2016 |
| Creators | Almeida, V?tor Alc?ntara de |
| Contributors | 00809085437, http://lattes.cnpq.br/2985658685449858, Costa, Umberto Souza da, 72031220500, http://lattes.cnpq.br/9526809466920084, Souza Neto, Pl?cido Antonio de, 01244350419, http://lattes.cnpq.br/3641504724164977, Bonichon, Richard Walter Alain, 00000000000, Deharbe, David Boris Paul |
| Publisher | Universidade Federal do Rio Grande do Norte, PROGRAMA DE P?S-GRADUA??O EM SISTEMAS E COMPUTA??O, UFRN, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0029 seconds