@MASTERSTHESIS{ 2024:455235698,
 	title = {Técnicas de contração de domínio de variáveis em verificação formal e detecção de vulnerabilidades de software usando programação por restrições e aritmética intervala},
 	year = {2024},
 	url = "https://tede.ufam.edu.br/handle/tede/10636",
 	abstract = "Nesta pesquisa são investigadas técnicas para resolução de problemas formulados para satisfazer um conjunto de restrições (Constraint Satisfaction Problems - CSP), modelados como expressões lógicas booleanas e cujas variáveis podem assumir valores reais, representando intervalos sobre os quais se aplica operações de aritmética intervalar e técnicas de programação por restrições (Constraint Programming - CP), para interseção, composição e contração de intervalos. Especificamente, o contexto de verificação formal de software é utilizado para a aplicação de redução do domínio de variáveis no pré-processamento de programas  que usam verificação formal para provar por meio das teorias de módulo da satisfatibilidade (Satisfiability Modulo Theories - SMT) a satisfabilidade ou não da fórmula booleana que representa todos os estados do programa. Foi utilizado, portanto, o método formal de verificação de modelo limitado (Bounded Model Checking - BMC),  que verifica em k passos se determinada propriedade é satisfatível ou, caso contrário, provê um contra-exemplo. Uma estratégia de pré-processamento BMC usando os programas modelados por CSP/CP e com soluções estimadas por uma técnica algorítmica de contração de intervalos é apresentada. Experimentos computacionais foram realizados usando benchmarks de programas em linguagem de programação C, Java e Kotlin, e utilizando o verificador ESBMC (e ESBMC-Jimple, desenvolvido no Projeto de PD&I SWPERFI UFAM-MOTOROLA, do qual esta pesquisa também faz parte) e outros. Os resultados indicam que, em muitos casos, há redução significativa do domínio das variáveis, influenciando na redução do espaço de busca exponencial da verificação de estados que, consequentemente, promove a diminuição do tempo de verificação  dos programas, mostrando a adequabilidade da estratégia proposta. Além disso, o método também foi empregado na detecção de vulnerabilidades de softwares, especificamente naquelas que podem envolver operações com intervalos aritméticos, alcançando resultados satisfatórios para a maioria das categorias de vulnerabilidades utilizadas.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de Pós-graduação em Informática},
 	note = {Instituto de Computação}
}