@MASTERSTHESIS{ 2021:234100466,
 	title = {Gera??o de casos de teste usando Bounded Model Checking},
 	year = {2021},
 	url = "https://tede.ufam.edu.br/handle/tede/8447",
 	abstract = "A gera??o autom?tica de casos de teste consiste na gera??o de entradas para um algoritmo que sejam capazes de explorar todos os caminhos de um programa, maximizando a cobertura. Comumente, t?cnicas como fuzzing s?o utilizadas para isso por sua performance alta e de custo baixo. Entretanto, t?cnicas formais, como execu??o simb?lica, v?m ganhando espa?o nesse dom?nio, entre elas, a Bounded Model Checking (BMC). BMC ? uma t?cnica de verifica??o que codifica uma propriedade em caminhos de um sistema de transi??o at? um limite k, resultando em uma ?nica f?rmula l?gica que, caso contenha uma viola??o, ir? gerar uma prova. Essa prova - embora reduzida - cont?m informa??es que podem ser utilizadas como base para a gera??o de um caso de teste. A dificuldade de usar BMC em casos de teste est? na complexidade de tempo/espa?o da t?cnica e nas simplifica??es feitas para tentar contornar isso (simplifica??es, estrat?gias). Incremental BMC ? uma estrat?gia que, de forma incremental, aumenta esse limite k at? que uma viola??o seja encontrada ou que o sistema seja completamente verificado. Entretanto, cada caminho do sistema ? reverificado a cada incremento, o que adiciona tempo e consumo de mem?ria para resolver a inst?ncia atual. Para resolver esses problemas, este trabalho prop?e duas contribui??es: (1) algoritmo de gera??o de casos de teste a partir de provas e (2) um sistema de cache que utiliza solu??es de inst?ncias menores atrav?s de (A) uso direto das inst?ncias anteriores; e (B) uso indireto atrav?s de f?rmulas de outros sistemas. Essas contribui??es foram implementadas no Efficient SMT-based Bounded Model Checker (ESBMC), sendo testadas em situa??es de Integra??o Cont?nua (CI) e sobre benchmarks p?blicos de programas em C, obtendo a primeira coloca??o na competi??o TestComp?21 na categoria reach-error e reduzindo o tempo do CI.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de P?s-gradua??o em Inform?tica},
 	note = {Instituto de Computa??o}
}