Advanced search options

Advanced Search Options 🞨

Browse by author name (“Author name starts with…”).

Find ETDs with:

in
/  
in
/  
in
/  
in

Written in Published in Earliest date Latest date

Sorted by

Results per page:

Dates: Last 2 Years

You searched for subject:(Mem ria). One record found.

Search Limiters

Last 2 Years | English Only

No search limiters apply to these results.

▼ Search Limiters

1. Sousa, Felipe Rodrigues Monteiro; http://lattes.cnpq.br/4475065926209027. Formal verification to ensuring the memory safety of C++ Programs.

Degree: 2020, Universidade Federal do Amazonas

In 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.

Este 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.

Advisors/Committee Members: Cordeiro, Lucas Carvalho, http://lattes.cnpq.br/5005832876603012, Barreto, Raimundo da Silva, http://lattes.cnpq.br/1132672107627968, Rocha, Herbert Oliveira, http://lattes.cnpq.br/2284500318304899.

Subjects/Keywords: Engenharia de Software; Software Verification; Model Checking; Memory Safety; Seguran?a de Mem?ria; CI?NCIAS EXATAS E DA TERRA: CI?NCIA DA COMPUTA??O: METODOLOGIA E T?CNICAS DA COMPUTA??O: ENGENHARIA DE SOFTWARE; Software Verification; Model Checking; C++; Memory Safety; Engenharia de Software; Verifica??o Formal; Seguran?a de Mem?ria

Record DetailsSimilar RecordsGoogle PlusoneFacebookTwitterCiteULikeMendeleyreddit

APA · Chicago · MLA · Vancouver · CSE | Export to Zotero / EndNote / Reference Manager

APA (6th Edition):

Sousa, F. R. M. h. c. b. (2020). Formal verification to ensuring the memory safety of C++ Programs. (Masters Thesis). Universidade Federal do Amazonas. Retrieved from https://tede.ufam.edu.br/handle/tede/7762

Chicago Manual of Style (16th Edition):

Sousa, Felipe Rodrigues Monteiro; http://lattes cnpq br/4475065926209027. “Formal verification to ensuring the memory safety of C++ Programs.” 2020. Masters Thesis, Universidade Federal do Amazonas. Accessed April 09, 2020. https://tede.ufam.edu.br/handle/tede/7762.

MLA Handbook (7th Edition):

Sousa, Felipe Rodrigues Monteiro; http://lattes cnpq br/4475065926209027. “Formal verification to ensuring the memory safety of C++ Programs.” 2020. Web. 09 Apr 2020.

Vancouver:

Sousa FRMhcb. Formal verification to ensuring the memory safety of C++ Programs. [Internet] [Masters thesis]. Universidade Federal do Amazonas; 2020. [cited 2020 Apr 09]. Available from: https://tede.ufam.edu.br/handle/tede/7762.

Council of Science Editors:

Sousa FRMhcb. Formal verification to ensuring the memory safety of C++ Programs. [Masters Thesis]. Universidade Federal do Amazonas; 2020. Available from: https://tede.ufam.edu.br/handle/tede/7762

.