@MASTERSTHESIS{ 2017:184273403,
 	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}
}