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

Esta dissertação descreve a fase inicial de um plugin para Frama-C e WP: o WPTrans. Ela é uma extensão que permite a manipulação, através de regras de inferência, das obrigações de prova geradas pelo WP, com a possibilidade de envio, em qualquer etapa da modi cação, a solucionadores SMT e outros provadores de teoremas. Algumas obrigações de prova podem ser validadas automaticamente, enquanto outras são muito complexas para os so- lucionadores SMT, exigindo uma prova manual pelo desenvolvedor, através dos assistentes de prova: esta abordagem geralmente requer do usuário uma experiência signi cativa 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 simpli car su cientemente as obrigações de prova para que possam ser validadas por qualquer outro solucionador SMT. Não obstante, a ferramenta é interligada diretamente ao WP, facilitando a instalação do plugin no Frama-C. Esta ferramenta também é uma porta de entrada para outras possíveis funcionalidades, sendo as mesmas discutidas neste documento.