Detalhes bibliográficos
| Ano de defesa: |
2016 |
| Autor(a) principal: |
Almeida, Vítor Alcântara de |
| Orientador(a): |
Deharbe, David Boris Paul |
| Banca de defesa: |
Não Informado pela instituição |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Universidade Federal do Rio Grande do Norte
|
| Programa de Pós-Graduação: |
PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO
|
| Departamento: |
Não Informado pela instituição
|
| País: |
Brasil
|
| Palavras-chave em Português: |
|
| Área do conhecimento CNPq: |
|
| Link de acesso: |
https://repositorio.ufrn.br/jspui/handle/123456789/21290
|
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. |
