???item.export.label??? ???item.export.type.endnote??? ???item.export.type.bibtex???

Please use this identifier to cite or link to this item: https://tede.ufam.edu.br/handle/tede/4497
???metadata.dc.type???: Dissertação
Title: Verificação baseada em indução matemática para programas C++
???metadata.dc.creator???: Gadelha, Mikhail Yasha Ramalho 
???metadata.dc.contributor.advisor1???: Cordeiro, Lucas Carvalho
???metadata.dc.description.resumo???: A utilização de sistemas embarcados, sistemas computacionais especializados para realizar uma função em sistemas maiores, eletrônicos ou mecânicos, vem crescendo no dia a dia das pessoas, e vem se tornando cada vez mais importante garantir a robustez desses sistemas. Existem diversas técnicas para garantir que um sistema seja lançado sem erros. Em especial, a verificação formal de programas está se mostrando efetiva na busca por falhas. Neste trabalho, serão descritos a verificação formal de programas C++ e a prova de corretude por indução matemática. Ambas as técnicas serão desenvolvidas utilizando a ferramenta Efficient SMTBased Context-Bounded Model Checker (ESBMC), um verificador de modelos que se baseia em teorias de satisfabilidade de fórmulas proposicionais e de lógica de primeira ordem. Os experimentos mostram que a ferramenta pode ser utilizada para verificar uma ampla gama de aplicações, de casos simples à aplicações comerciais. A ferramenta também mostrou-se superior em comparação com outros verificadores na verificação de programas C++, encontrando um maior número de erros e suportando um número superior das funcionalidades que a linguagem C++ tem a oferecer, além de ser capaz de provar diversas propriedades (por exemplo, laços invariantes), utilizando a técnica de indução matemática.
Abstract: The use of embedded systems, computational systems specialized to do a function in larger systems, electronic or mechanical, is growing in the daily life, and it is becoming increasingly important to ensure the robustness of these systems. There are several techniques to ensure that a system is released without error. In particular, formal verification is proving very effective in finding bugs in programs. In this work, we describe the formal verification for C++ Programs and correctness proof by mathematical induction. Both techniques will be developed using the tool Efficient SMT-Based Context-Bounded Model Checker (ESBMC), a model checker based on satisfiability modulo theories and first order logic. The experiments show that the tool can be used to check a wide range of applications, from simple test cases to commercial applications. The tool also proved to be more efficient than other models checkers to verify C++ programs, finding a greater number of bugs, and supporting a larger number of the features that the language C++ has to offer, in addition to being able to prove several properties, using the method of mathematical induction.
Keywords: Verificação formal
Prova por indução
Linguagem de programação C++
Formal verification
Proof by induction
C++ programming language
???metadata.dc.subject.cnpq???: ENGENHARIAS: ENGENHARIA ELÉTRICA
Language: por
???metadata.dc.publisher.country???: Brasil
Publisher: Universidade Federal do Amazonas
???metadata.dc.publisher.initials???: UFAM
???metadata.dc.publisher.department???: Faculdade de Tecnologia
???metadata.dc.publisher.program???: Programa de Pós-graduação em Engenharia Elétrica
Citation: GADELHA, Mikhail Yasha Ramalho. Verificação baseada em indução matemática para programas C++. 2013. 85 f. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Manaus, 2013.
???metadata.dc.rights???: Acesso Aberto
URI: http://tede.ufam.edu.br/handle/tede/4497
Issue Date: 20-Dec-2013
Appears in Collections:Mestrado em Engenharia Elétrica

Files in This Item:
File Description SizeFormat 
Dissertação - Mikhail Yasha Ramalho Gadelha.pdfDissertação - Mikhail Yasha Ramalho Gadelha1.8 MBAdobe PDFThumbnail

Download/Open Preview


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.