Defect Detection: Combining Bounded Model Checking and Code Contracts
| Autor: | Marat Akhin, Mikhail Belyaev, Vladimir Itsykson |
|---|---|
| Jazyk: | English<br />Russian |
| Rok vydání: | 2013 |
| Předmět: | |
| Zdroj: | Моделирование и анализ информационных систем, Vol 20, Iss 6, Pp 22-35 (2013) |
| Druh dokumentu: | article |
| ISSN: | 1818-1015 2313-5417 |
| DOI: | 10.18255/1818-1015-2013-6-22-35 |
| Popis: | 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 model generation, employment of high-performance Z3 SMT solver to do the formula heavy-lifting, and the use of various function summaries to improve analysis efficiency and expressive power. We have implemented a basic prototype; experiment results on a set of simple test BMC problems are satisfactory. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|