Formal Verification to Ensuring the Memory Safety of C++ Programs
- 2020 M.Sc. Thesis; Felipe R. Monteiro
- Apply model checking techniques to ensuring memory safety of C++ programs:
- (i) Provide a logical formalization of essential features that the C++ programming language offers, such as templates, sequential and associative containers, inheritance, polymorphism, and exception handling.
- (ii) Provide a set of abstractions to the Standard C++ Libraries that reflects their semantics, in order to enable the verification of functional properties related to the use of these libraries.
- (iii) Extend an existing verifier to handle the verification of C++ programs based on (i) and (ii) and evaluate its efficiency and effectiveness in comparison to similar state-of-the-art approaches.
Model Checking a C++ Software Framework, a Case Study
Last modified 06 April 2022