@MASTERSTHESIS{ 2011:1571505579,
 	title = {Verifica??o e comprova??o de erros em c?digos C usando bounded model checker},
 	year = {2011},
 	url = "http://tede.ufam.edu.br/handle/tede/2965",
 	abstract = "A utiliza??o de sistemas baseados em computador em diversos dom?nios aumentou
 significativamente nos ?ltimos anos. Um dos principais desafios no desenvolvimento
 de software de sistemas cr?ticos ? a garantia da sua corre??o e confiabilidade. Desta
 forma, a verifica??o de software exerce um papel importante para assegurar a qualidade
 geral do produto, visando principalmente caracter?sticas como previsibilidade e confiabilidade.
 No contexto de verifica??o de software, os Bounded Model Checkers est?o
 sendo utilizados para descobrir erros sutis em projetos de sistemas de software atuais,
 contribuindo eficazmente neste processo de verifica??o. O valor dos contra-exemplos e
 propriedades de seguran?a gerados pelo Bounded Model Checkers para criar casos de
 testes e para a depura??o de sistemas ? amplamente reconhecido. Quando um Bounded
 Model Checking (BMC) encontra um erro ele produz um contra-exemplo. Assim,
 o valor dos contra-exemplos para depura??o de software ? amplamente reconhecido no
 estado da pr?tica. Entretanto, os BMCs frequentemente produzem contra-exemplos
 que s?o grandes ou dif?ceis de entender ou manipular, principalmente devido ao tamanho
 do software e valores escolhidos pelo solucionador de satisfabilidade. Neste
 trabalho visamos demonstrar e analisar o uso de m?todo formal (atrav?s da t?cnica
 model checking) no processo de desenvolvimento de programas na linguagem C, explorando
 as caracter?sticas j? providas pelo model checking como o contra-exemplo e a
 identifica??o e verifica??o de propriedades de seguran?a. Em face disto apresentamos
 duas abordagens: (i) descrevemos um m?todo para integrar o Bounded Model Checker
 ESBMC como o framework de teste unit?rio CUnit, este m?todo visa extrair as
 propriedades geradas pelo ESBMC para gerar automaticamente casos de teste usando
 o rico conjunto de assertivas providas pelo framework CUnit e (ii) um m?todo que
 visa automatizar a coleta e manipula??o dos contra-exemplos, de modo a instanciar o
 programa C analisado, para comprovar a causa raiz do erro identificado. Tais m?todos
 podem ser vistos como um m?todo complementar para a verifica??o efetuada pelos
 BMCs. Demonstramos a efic?cia dos m?todos propostos sobre benchmarks p?blicos de
 c?digo C.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de P?s-gradua??o em Inform?tica},
 	note = {Instituto de Computa??o}
}