Frama-C, WP, WPTrans, Obrigação de Prova, Coq, SMT. 

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, das
obrigaçõ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. Algumas
obrigações de prova podem ser validadas automaticamente, enquanto outras são muito
complexas para os solucionadores SMT, exigindo uma prova manual pelo desenvolvedor,
através dos assistentes de prova. Contudo, a segunda abordagem geralmente requer do
usuário uma experiência significativa 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 simplificar suficientemente as obrigações de
prova para que possam ser validadas por qualquer outro solucionador SMT.
Não obstante, a extensão é interligada diretamente ao WP, facilitando a instalação do
plugin no Frama-C. Esta extensão também é uma porta de entrada para outras possíveis
funcionalidades, sendo as mesmas discutidas neste documento.