1. TEDE
  2. Unidade Manaus
  3. Programa de Pós-graduação em Informática
  4. Mestrado em Informática
???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/7762
Full metadata record
DC FieldValueLanguage
dc.creatorSousa, Felipe Rodrigues Monteiro-
dc.creator.Latteshttp://lattes.cnpq.br/4475065926209027por
dc.contributor.advisor1Cordeiro, Lucas Carvalho-
dc.contributor.advisor1Latteshttp://lattes.cnpq.br/5005832876603012por
dc.contributor.referee1Barreto, Raimundo da Silva-
dc.contributor.referee1Latteshttp://lattes.cnpq.br/1132672107627968por
dc.contributor.referee2Rocha, Herbert Oliveira-
dc.contributor.referee2Latteshttp://lattes.cnpq.br/2284500318304899por
dc.date.issued2020-01-17-
dc.identifier.citationMONTEIRO, Felipe Rodrigues Monteiro. Formal verification to ensuring the memory safety of C++ Programs. 2020. 71 f. Dissertação (Mestrado em Informática) - Universidade Federal do Amazonas, Manaus, 2020.por
dc.identifier.urihttps://tede.ufam.edu.br/handle/tede/7762-
dc.description.resumoIn the last three decades, memory safety issues in low-level programming languages such as C or C++ have been one of the significant sources of security vulnerabilities; however, there exist only a few attempts with limited success to cope with the complexity of C++ program verification. This work describes and evaluates a novel verification approach based on bounded model checking (BMC) and satisfiability modulo theories (SMT) to verify C++ programs formally. This verification approach analyzes bounded C++ programs by encoding various sophisticated features that the C++ programming language offers into SMT, such as templates, sequential and associative containers, inheritance, polymorphism, and exception handling. We formalize these sophisticated features within our formal verification framework using a decidable fragment of first-order logic and then show how state-of-the-art SMT solvers can efficiently handle that. We implemented this verification approach on top of the Efficient SMT-Based Context-Bounded Model Checker (ESBMC). We compare ESBMC to LLBMC and DIVINE, which are state-of-the-art verifiers to check C++ programs directly from LLVM bitcode. The experimental evaluation contains a set of over 1,500 benchmarks from several sources (e.g., Deitel & Deitel, NEC Corporation, and GCC test suite), which covers several C++ features. Experimental results show that ESBMC can handle a wide range of C++ programs, presenting a higher number of correct verification results, and at the same time, it reduces the verification time if compared to LLBMC and DIVINE tools.por
dc.description.abstractEste trabalho descreve e avalia o Efficient SMT-Based Context-Bounded Model Checker (ESBMC) para verificar formalmente programas C++. O ESBMC implementa a técnica de verificação de modelos limitados (do inglês, bounded model checking -- BMC) com base em teorias do módulo da satisfabilidade (do inglês, satisfiability modulo theories -- SMT) para lidar com recursos complexos que a linguagem de programação C++ oferece, tais como templates, contêineres sequenciais e associativos, herança, polimorfismo e manipulação de exceções. ESBMC é comparado as ferramentas LLBMC e DIVINE, as quais verificam os programas C++ diretamente a nível de bitcode do LLVM. Resultados experimentais mostram que o ESBMC pode lidar com uma ampla gama de estruturas do C++, apresentando uma taxa de aproximadamente 85% de verificações corretas e, ao mesmo tempo, reduzindo o tempo de verificação se comparado as ferramentas LLBMC e DIVINE.por
dc.formatapplication/pdf*
dc.thumbnail.urlhttps://tede.ufam.edu.br//retrieve/38459/Disserta%c3%a7%c3%a3o_FelipeRodriguesMonteiro_PPGI.pdf.jpg*
dc.languageengpor
dc.publisherUniversidade Federal do Amazonaspor
dc.publisher.departmentInstituto de Computaçãopor
dc.publisher.countryBrasilpor
dc.publisher.initialsUFAMpor
dc.publisher.programPrograma de Pós-graduação em Informáticapor
dc.rightsAcesso Abertopor
dc.rights.urihttp://creativecommons.org/licenses/by/4.0/-
dc.subjectEngenharia de Softwarepor
dc.subjectSoftware Verificationpor
dc.subjectModel Checkingpor
dc.subjectMemory Safetypor
dc.subjectSegurança de Memóriapor
dc.subject.cnpqCIÊNCIAS EXATAS E DA TERRA: CIÊNCIA DA COMPUTAÇÃO: METODOLOGIA E TÉCNICAS DA COMPUTAÇÃO: ENGENHARIA DE SOFTWAREpor
dc.titleFormal verification to ensuring the memory safety of C++ Programspor
dc.title.alternativeVerificação formal de programas C++ para garantir segurança de memóriapor
dc.typeDissertaçãopor
dc.contributor.advisor1orcidhttps://orcid.org/0000-0002-6235-4272por
dc.creator.orcidhttps://orcid.org/0000-0001-9420-9056por
dc.contributor.referee2orcidhttps://orcid.org/0000-0002-2648-8468por
dc.subject.userSoftware Verificationeng
dc.subject.userModel Checkingeng
dc.subject.userC++eng
dc.subject.userMemory Safetyeng
dc.subject.userEngenharia de Softwarepor
dc.subject.userVerificação Formalpor
dc.subject.userSegurança de Memóriapor
Appears in Collections:Mestrado em Informática

Files in This Item:
File Description SizeFormat 
Dissertação_FelipeRodriguesMonteiro_PPGI.pdfDissertação_FelipeRodriguesMonteiro_PPGI1.68 MBAdobe PDFThumbnail

Download/Open Preview
Show simple item record Recommend this item


This item is licensed under a Creative Commons License Creative Commons