Defect Detection: Combining Bounded Model Checking and Code Contracts

<p>Bounded model checking (BMC) of C/C++ programs is a matter of scientific enquiry that attracts great attention in the last few years. In this paper, we present our approach to this problem. It is based on combining several recent results in BMC, namely, the use of LLVM as a baseline for mod...

Full description

Bibliographic Details
Main Authors: Marat Akhin, Mikhail Belyaev, Vladimir Itsykson
Format: Article
Language:English
Published: Yaroslavl State University 2013-01-01
Series:Моделирование и анализ информационных систем
Subjects:
Online Access:http://mais-journal.ru/jour/article/view/155