Verificação baseada em indução matemática para programas C++

• Ano de defesa: 2013
• Autor(a) principal: Gadelha, Mikhail Yasha Ramalho
• Outros Autores: http://lattes.cnpq.br/5172660162494409
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal do Amazonas; Faculdade de Tecnologia; Brasil; UFAM; Programa de Pós-graduação em Engenharia Elétrica
• Palavras-chave em Português: Verificação formal; Prova por indução; Linguagem de programação C++; Formal verification; Proof by induction; C++ programming language; ENGENHARIAS: ENGENHARIA ELÉTRICA
• Link de acesso: http://tede.ufam.edu.br/handle/tede/4497

A utilização de sistemas embarcados, sistemas computacionais especializados para realizar uma função em sistemas maiores, eletrônicos ou mecânicos, vem crescendo no dia a dia das pessoas, e vem se tornando cada vez mais importante garantir a robustez desses sistemas. Existem diversas técnicas para garantir que um sistema seja lançado sem erros. Em especial, a verificação formal de programas está se mostrando efetiva na busca por falhas. Neste trabalho, serão descritos a verificação formal de programas C++ e a prova de corretude por indução matemática. Ambas as técnicas serão desenvolvidas utilizando a ferramenta Efficient SMTBased Context-Bounded Model Checker (ESBMC), um verificador de modelos que se baseia em teorias de satisfabilidade de fórmulas proposicionais e de lógica de primeira ordem. Os experimentos mostram que a ferramenta pode ser utilizada para verificar uma ampla gama de aplicações, de casos simples à aplicações comerciais. A ferramenta também mostrou-se superior em comparação com outros verificadores na verificação de programas C++, encontrando um maior número de erros e suportando um número superior das funcionalidades que a linguagem C++ tem a oferecer, além de ser capaz de provar diversas propriedades (por exemplo, laços invariantes), utilizando a técnica de indução matemática.