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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2013-01-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | http://mais-journal.ru/jour/article/view/155 |
| _version_ | 1797967108164812800 |
|---|---|
| author | Marat Akhin Mikhail Belyaev Vladimir Itsykson |
| author_facet | Marat Akhin Mikhail Belyaev Vladimir Itsykson |
| author_sort | Marat Akhin |
| collection | DOAJ |
| description | <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 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. </p> |
| first_indexed | 2024-04-11T02:26:00Z |
| format | Article |
| id | doaj.art-7f96f0885b404eff9c1be3d6a5afa141 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-11T02:26:00Z |
| publishDate | 2013-01-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-7f96f0885b404eff9c1be3d6a5afa1412023-01-02T22:40:48ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172013-01-012062235149Defect Detection: Combining Bounded Model Checking and Code ContractsMarat Akhin0Mikhail Belyaev1Vladimir Itsykson2Санкт-Петербургский государственный политехнический университетСанкт-Петербургский государственный политехнический университетСанкт-Петербургский государственный политехнический университет<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 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. </p>http://mais-journal.ru/jour/article/view/155ограниченная проверка моделейконтракт кодаинтерполяция КрейгаSMTобнаружение ошибок |
| spellingShingle | Marat Akhin Mikhail Belyaev Vladimir Itsykson Defect Detection: Combining Bounded Model Checking and Code Contracts Моделирование и анализ информационных систем ограниченная проверка моделей контракт кода интерполяция Крейга SMT обнаружение ошибок |
| title | Defect Detection: Combining Bounded Model Checking and Code Contracts |
| title_full | Defect Detection: Combining Bounded Model Checking and Code Contracts |
| title_fullStr | Defect Detection: Combining Bounded Model Checking and Code Contracts |
| title_full_unstemmed | Defect Detection: Combining Bounded Model Checking and Code Contracts |
| title_short | Defect Detection: Combining Bounded Model Checking and Code Contracts |
| title_sort | defect detection combining bounded model checking and code contracts |
| topic | ограниченная проверка моделей контракт кода интерполяция Крейга SMT обнаружение ошибок |
| url | http://mais-journal.ru/jour/article/view/155 |
| work_keys_str_mv | AT maratakhin defectdetectioncombiningboundedmodelcheckingandcodecontracts AT mikhailbelyaev defectdetectioncombiningboundedmodelcheckingandcodecontracts AT vladimiritsykson defectdetectioncombiningboundedmodelcheckingandcodecontracts |