Defect Detection: Combining Bounded Model Checking and Code Contracts
https://doi.org/10.18255/1818-1015-2013-6-22-35
Abstract
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.
About the Authors
Marat Akhin
Saint-Petersburg State Polytechnical University
Russian Federation
Russian Federation
аспирант,
Polytechnicheskaya street, 21, Saint-Petersburg 194021 Russia
Mikhail Belyaev
Saint-Petersburg State Polytechnical University
Russian Federation
Russian Federation
аспирант,
Polytechnicheskaya street, 21, Saint-Petersburg 194021 Russia
Vladimir Itsykson
Saint-Petersburg State Polytechnical University
Russian Federation
Russian Federation
доцент,
Polytechnicheskaya street, 21, Saint-Petersburg 194021 Russia
References
1. Clarke E., Kroening D., Lerda F. A Tool for Checking ANSI-C Programs // TACAS ’04. Springer-Verlag, 2004. P. 168–176.
2. Armando A., Mantovani J., Platania L. Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers // Int. J. Softw. Tools Technol. Transf. Springer-Verlag, 2009. 11, 1. P. 69–83.
3. Cordeiro L., Fischer B., Marques-Silva J. SMT-Based Bounded Model Checking for Embedded ANSI-C Software // ASE ’09. IEEE. 2009. P. 137–148.
4. Merz F., Falke S., Sinz C. LLBMC: Bounded Model Checking of C and C++ Programs using a Compiler IR // VSTTE ’12. Springer-Verlag, 2012. P. 146–161.
5. Ицыксон В.М., Глухих М.И. Язык спецификаций поведения программных компонентов // Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление. 3. СПб: СПбГПУ, 2010. С. 63–71. (Itsykson V., Glukhikh M. Yazyk specifikaciy povedeniya programmnyh komponentov // Nauchno-tehnicheskie vedomosti SPbGPU. Informatika. Telekommunikacii. Upravlenie. 3. SPb: SPbGPU, 2010. P. 63–71 [in Russian]).
6. Ицыксон В. М., Зозуля А. В. Автоматизированная трансформация программ при миграции на новые библиотеки // Программная инженерия. 6. М: Новые Технологии, 2012 С. 8–14. (English transl.: Itsykson V., Zozulya A. Automated Program Transformation for Migration to New Libraries // SECR ’11. IEEE, 2011. P. 1–7).
7. Baudin P., Filliˆatre J.C., Hubert T., March´e C., Monate B., Moy Y., Prevosto V. ACSL: ANSI/ISO C Specification Language. Preliminary Design, Version 1.4, 2008. http://www.frama-c.cea.fr/download/acsl_1.4.pdf
8. Sery O., Fedyukovich G., Sharygina N. Interpolation-Based Function Summaries in Bounded Model Checking // HVC ’11. Springer-Verlag, 2011. P. 160–175.
9. Biere A., Cimatti A., Clarke E. M., Zhu Y. Symbolic Model Checking without BDDs // TACAS ’99. Springer-Verlag, 1999. P. 193–207.
10. Barrett C., Sebastiani R., Seshia S.A., Tinelli C. Satisfiability Modulo Theories // Handbook of Satisfiability. 185. Frontiers in Artificial Intelligence and Applications, 2009. P. 825–885.
11. Lattner C., Adve V. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation // CGO ’04. IEEE, 2004. P. 75–86.
12. Cytron R., Ferrante J., Rosen B.K., Wegman M.N., Zadeck F.K. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph // ACM TOPLAS. 1991. 13, 4. P. 451–490.
13. McMillan K.L. Applications of Craig Interpolants in Model Checking // TACAS ’05. Springer-Verlag, 2005. P. 1–12.
14. Craig W. Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory // The Journal of Symbolic Logic. 22, 3. Association for Symbolic Logic, 1957. P. 269–285.
15. De Moura L., Bjørner N. Z3: An Efficient SMT Solver // TACAS ’08. Springer-Verlag, 2008. P. 337–340.
16. Barrett C., De Moura L., Stump A. SMT-COMP: Satisfiability Modulo Theories Competition // CAV ’05. Springer-Verlag, 2005. P. 503–516.
17. Cok D.R., Griggio A., Bruttomesso R. The 2012 SMT Competition. 2012. http://smtcomp.sourceforge.net/2012/
18. Coverity. Open Source Report 2011. http://www.coverity.com/library/pdf/coverity-scan-2011-open-source-integrity-report.pdf
19. NEC Laboratories. NECLA Static Analysis Benchmarks. 2013. http://www.nec-labs.com/research/system/systems_SAV-website/benchmarks.php
Review
For citations:
Akhin M., Belyaev M., Itsykson V. Defect Detection: Combining Bounded Model Checking and Code Contracts. Modeling and Analysis of Information Systems. 2013;20(6):22-35. (In Russ.) https://doi.org/10.18255/1818-1015-2013-6-22-35
Views:
1107
Email this article 