@PHDTHESIS{ 2015:178253040,
 	title = {Veri?ca??o de sistemas de software baseada em transforma??es de c?digo usando Bounded Model Checking},
 	year = {2015},
 	url = "http://tede.ufam.edu.br/handle/tede/4752",
 	abstract = "Um dos principais desa?os no desenvolvimento de software ? garantir a funcionalidade dos
 sistemas de software, especialmente em sistemas embarcados cr?ticos, tais como aeron?utico ou
 hospitalar, onde diversas restri??es (por exemplo, tempo de resposta e precis?o dos dados) devem
 ser atendidas e mensuradas de acordo com os requisitos do usu?rio, caso contr?rio uma falha pode
 conduzir a situa??es catastr??cas. Logo, t?cnicas de veri?ca??o e teste de software s?o itens
 indispens?veis para um desenvolvimento com qualidade, onde tais t?cnicas visam con?rmar os
 requisitos do usu?rio, bem como os comportamentos pr?-estabelecidos para osoftware.
 No contexto de veri?ca??o de software, visando ? qualidade geral do produto, a t?cnica de
 veri?ca??o formal model checking tem sido utilizada para descobrir erros sutis em projetos de
 sistemas de software atuais. Contudo, a utiliza??o da t?cnica model checking apresenta alguns
 desa?os, tais como, lidar com a explos?o do espa?o de estados do modelo, integra??o com outros
 ambientes de testes mais familiares aos projetistas e tratamento e an?lise de contra-exemplos para
 reprodu??o de erros. De modo a lidar com estes problemas, uma poss?vel solu??o ? explorar as
 caracter?sticas j? providas pelos model checkers, por exemplo, a veri?ca??o de propriedades de
 seguran?a e gera??o de contra-exemplos. Explorando este conjunto de caracter?sticas, juntamente
 com autiliza??o dainfer?ncia deinvariantes eumtipo especial demodelchecking, denominado de
 BoundedModelChecking (BMC),esta tese apresenta um conjunto de m?todos para complementar
 e aprimorar a escalabilidade e acur?cia da veri?ca??o efetuada por Bounded Model Checkers.
 Estes m?todos utilizam t?cnicas de transforma??es de c?digo para explorar as caracter?sticas de
 Bounded Model Checkers, a ?m de analisar propriedades de seguran?a e demonstrar erros em
 c?digos escritos na linguagem de programa??o C.
 Os m?todos apresentados nesta tese s?o: (1) A gera??o e veri?ca??o autom?tica de casos de teste
 baseado em propriedades de seguran?a geradas por um Bounded Model Checker para testes de
 unidade; (2) Automatizar acoleta emanipula??o das informa??es dos contra-exemplos, de modo a
 demonstrar a causa principal do erro identi?cado; e (3) Utiliza??o de invariantes
 dinamicamente/estaticamente inferidas, a partir do programa analisado, para restringir a
 explora??o dos conjuntos de estados durante a execu??o da veri?ca??o pelo BMC. Desta forma,
 ajudando no aprimoramento da veri?ca??o efetuada por um BMC, no que concerne em auxiliar a
 sua veri?ca??o e na precis?o dos resultados, pela utiliza??o de invariantes de programas. As
 abordagens propostas, quando utilizadas isoladamente, fornecem alternativas complementares a
 veri?ca??o e, interligadas, aprimoram a veri?ca??o de c?digo. Os resultados experimentais dos
 m?todos propostos demonstram ser e?cientes sobre benchmarks p?blicos de programas em C,
 encontrando defeitos n?o anteriormente encontrados por outros m?todos que s?o estado-da-arte.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de P?s-gradua??o em Inform?tica},
 	note = {Instituto de Computa??o}
}