Projects per year
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
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 language | English |
|---|---|
| Title of host publication | 15th IEEE International Conference on Software Testing, Verification and Validation (ICST) 2022 |
| Publication status | Accepted/In press - 6 Jan 2022 |
Fingerprint
Dive into the research topics of 'Summary of Model Checking C++ Programs'. Together they form a unique fingerprint.-
EnnCore: End-to-End Conceptual Guarding of Neural Architectures
Cordeiro, L. (PI), Brown, G. (CoI), Freitas, A. (CoI), Luján, M. (CoI) & Mustafa, M. (CoI)
1/02/21 → 31/12/25
Project: Research
-
SCorCH: Secure Code for Capability Hardware
Reger, G. (PI), Cordeiro, L. (CoI), Korovin, K. (CoI), Mustafa, M. (CoI) & Olivier, P. (CoI)
1/07/20 → 31/12/23
Project: Research