@MASTERSTHESIS{ 2019:2009827924,
 	title = {Uma abordagem de otimização guiada por contraexemplos usando solucionadores SAT e SMT},
 	year = {2019},
 	url = "https://tede.ufam.edu.br/handle/tede/7096",
 	abstract = "O processo de otimização exige uma formulação matemática do sistema ou problema a
 ser otimizado, e considerando que os métodos formais são técnicas baseadas nos formalismos
 matemáticos usados para a especificação, desenvolvimento e verificação de sistemas, busca-se
 usar métodos formais para a otimização de funções matemáticas.
 Este trabalho apresenta o desenvolvimento da ferramenta de otimização guiada por
 contraexemplos OptCE, assim como os algoritmos de otimização indutiva guiada por
 contraexemplos (CEGIO). Busca-se estabelecer o uso da verificação de modelos limitados
 para a otimização em funções convexas e não convexas, encapsulando a metodologia em uma
 ferramenta, permitindo uma otimização guiada a partir de contraexemplos dos solucionadores
 de Satisfatibilidade Booleana (Boolean Satisfiability - SAT) e Teoria do Módulo de
 Satisfatibilidade (Satisfiability Modulo Theories - SMT).
 Durante o trabalho é detalhado a metodologia e exemplo para uma otimização guiada
 por contraexemplos, assim como os algoritmos CEGIO, que têm como objetivo a localização
 do mínimo global em uma função.
 Também são apresentados o desenvolvimento,
 funcionalidades e avaliação da ferramenta de otimização OptCE. O usuário fornece um arquivo
 com a modelagem da função e suas restrições, e o OptCE usa as informações para implementar
 os algoritmos CEGIO, inserir propriedades, aplicar verificadores de programas para checar
 propriedades, gerar contraexemplos SAT e SMT, executando de forma automatizada as etapas
 de especificação e verificação sucessivas vezes em busca do ponto ótimo da função.
 A avaliação do OptCE foi realizada a partir de funções de otimização obtidas da
 literatura, e foram comparadas com outras técnicas tradicionais. Os experimentos utilizaram
 40 funções (convexas e não convexas) onde os resultados obtidos mostram sua capacidade de
 otimização, tendo melhor taxa de acerto quando comparada com as técnicas.",
 	publisher = {Universidade Federal do Amazonas},
 	scholl = {Programa de Pós-graduação em Engenharia Elétrica},
 	note = {Faculdade de Tecnologia}
}