@MASTERSTHESIS{ 2017:1869170349,
 	title = {Verificação de Programas Embarcados ANSI-C baseada em indução Matemática e Invariantes},
 	year = {2017},
 	url = "https://tede.ufam.edu.br/handle/tede/6261",
 	abstract = "O uso de sistemas embarcados, sistemas computacionais especializados para execução
 em sistemas eletrônicos ou mecânicos tem crescido de forma vertiginosa devido a utilização
 cada vez mais intensa de sensores, interfaces de rede e protocolos de comunicação em diversas
 áreas. Por isso, é cada vez mais importante garantir a robustez desses sistemas, uma vez
 que estão se tornando mais complexos e integrados. Existem várias técnicas para garantir que
 um sistema seja entregue ao cliente sem erros, em particular, a verificação formal dos programas
 tem se revelado eficaz na busca de falhas. Neste trabalho é descrito um algoritmo de
 indução matemática conhecido como k-induction combinado ao uso de invariantes para verificar
 e refutar propriedades de segurança em programas desenvolvidos na linguagem ANSI-C.
 Em particular, a abordagem proposta infere invariantes no programa para auxiliar na verificação
 de programas ANSI-C através da técnica de indução matemática através do refinamento
 de restrição (i.e, poliédrico) para especificar pré- e pós-condições.
 No método proposto, adotamos dois geradores de invariantes para produzir e alimentar
 o algoritmo de indução matemática o qual é implementado na ferramenta Efficient SMT-Based
 Context-Bounded Model Checker. A motivação para a combinação de invariantes com o algoritmo
 de indução matemática é fechar um gap na verificação formal de programas que possuam
 variáveis globais, além de programas com loops que possuem desvios condicionais e o número
 de iterações é desconhecido. PIPS e PAGAI são as ferramentas utilizadas para analisar o código
 e produzir invariantes indutivas responsáveis por guiar o algoritmo de indução matemática na
 verificação do benchmark, sendo este o principal desafio do método proposto.
 Para avaliar a eficácia da abordagem proposta neste trabalho, além de aplicações de
 Sistemas Embarcados foram utilizados benchmarks públicos disponibilizados pela Competição
 Internacional de Verificação de Software onde participam Universidades, pesquisadores, estudandantes
 de doutorado de várias partes do mundo, e fornece amplo conjunto de casos de teste
 para verificação. Além disso, foram utilizadas ferramentas estado-da-arte para a comparação
 dos resultados e, assim mensurar a eficácia do método proposto.
 Os resultados experimentais foram positivos e mostraram que o algoritmo de indução
 matemática com invariantes pode verificar uma grande variedade de propriedades de segurança
 em programas com loops e aplicações de sistemas embarcados de telecomunicações, sistemas
 de controle e dispositivos médicos.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de Pós-graduação em Engenharia Elétrica},
 	note = {Faculdade de Tecnologia}
}