@PHDTHESIS{ 2015:1327735776,
 	title = {Verificaçã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 desafios 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óficas. Logo, técnicas de verificação e teste de software são itens
 indispensáveis para um desenvolvimento com qualidade, onde tais técnicas visam confirmar os
 requisitos do usuário, bem como os comportamentos pré-estabelecidos para osoftware.
 No contexto de verificação de software, visando à qualidade geral do produto, a técnica de
 verificaçã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
 desafios, 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 verificaçã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 verificaçã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 fim 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 verificaçã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 identificado; 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 verificação pelo BMC. Desta forma,
 ajudando no aprimoramento da verificação efetuada por um BMC, no que concerne em auxiliar a
 sua verificação e na precisão dos resultados, pela utilização de invariantes de programas. As
 abordagens propostas, quando utilizadas isoladamente, fornecem alternativas complementares a
 verificação e, interligadas, aprimoram a verificação de código. Os resultados experimentais dos
 métodos propostos demonstram ser eficientes 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}
}