Summary of Model Checking C++ Programs

Felipe R. Monteiro, Mikhail R Gadelha, Lucas C. Cordeiro

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

This is an extended abstract of the article “Model Checking C++ Programs” by Felipe R. Monteiro, Mikhail R. Gadelha, and Lucas C. Cordeiro. We describe and evaluate a
novel verification approach based on bounded model checking (BMC) and satisfiability modulo theories (SMT) to verify C++ programs. Our verification approach analyzes bounded C++ programs by encoding into SMT various sophisticated features that the C++ programming language offers, such as templates, inheritance, polymorphism, exception handling, and the Standard
Template Libraries. We implemented our verification approach on top of ESBMC. We compare ESBMC to LLBMC and DIVINE, which are state-of-the-art verifiers to check C++ programs directly from the LLVM bitcode. Experimental results show that
ESBMC can handle a wide range of C++ programs, presenting a higher number of correct verification results. Additionally, ESBMC has been applied to a commercial C++ application in the telecommunication domain and successfully detected arithmeticoverflow errors, which could lead to security vulnerabilities.

Index Terms—C++, memory safety, model checking, SMT, software verification
Original languageEnglish
Title of host publication15th IEEE International Conference on Software Testing, Verification and Validation (ICST) 2022
Publication statusAccepted/In press - 6 Jan 2022

Fingerprint

Dive into the research topics of 'Summary of Model Checking C++ Programs'. Together they form a unique fingerprint.

Cite this