WPTrans: um assistente para verificação de programas em Frama-C - Almeida, Vítor Alcântara de (2016)
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.