Name
Title | ||
|---|---|---|
Software defect detection by combining bounded model checking and approximations of functions. |
Abstract | ||
|---|---|---|
In recent years, the study of a software quality assurance technique called bounded model checking (BMC) has been increasingly intensified, because it makes it possible to successfully detect both functional and nonfunctional defects in real software. In this paper, we propose an original approach to the implementation of BMC based on combining the results of several recent studies in this field, namely, the use of the LLVM compiler infrastructure for parsing and transformation of the source code, the use of SMT-solver Z3 for the verification of the correctness of the properties, and the improvement of the analysis efficiency using the approximation of functions. The experimental results show that the approach can be applied to real projects. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.3103/S0146411614070025 | Automatic Control and Computer Sciences |
Keywords | Field | DocType |
bounded model checking, code contracts, Craig interpolation, SMT, error detection | Model checking,Source code,Computer science,Correctness,Software bug,Theoretical computer science,Compiler,Software quality assurance,Software,Bounded function | Journal |
Volume | Issue | ISSN |
48 | 7 | 1558-108X |
Citations | PageRank | References |
2 | 0.43 | 10 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marat Kh. Akhin | 1 | 2 | 0.76 |
| Mikhail A. Belyaev | 2 | 2 | 1.10 |
| Vladimir Itsykson | 3 | 3 | 2.50 |