Geodesic
Defect Detection: Combining Bounded Model Checking and Code Contracts
Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 6, pp. 22-35.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: bounded model checking, satisfiability modulo theories, LLVM, function contracts, function summaries. 
@article{MAIS_2013_20_6_a1,
     author = {Marat Akhin and Mikhail Belyaev and Vladimir Itsykson},
     title = {Defect {Detection:} {Combining} {Bounded} {Model} {Checking} and {Code} {Contracts}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {22--35},
     publisher = {mathdoc},
     volume = {20},
     number = {6},
     year = {2013},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a1/}
}
TY  - JOUR
AU  - Marat Akhin
AU  - Mikhail Belyaev
AU  - Vladimir Itsykson
TI  - Defect Detection: Combining Bounded Model Checking and Code Contracts
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2013
SP  - 22
EP  - 35
VL  - 20
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a1/
LA  - ru
ID  - MAIS_2013_20_6_a1
ER  - 
%0 Journal Article
%A Marat Akhin
%A Mikhail Belyaev
%A Vladimir Itsykson
%T Defect Detection: Combining Bounded Model Checking and Code Contracts
%J Modelirovanie i analiz informacionnyh sistem
%D 2013
%P 22-35
%V 20
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a1/
%G ru
%F MAIS_2013_20_6_a1
Marat Akhin; Mikhail Belyaev; Vladimir Itsykson. Defect Detection: Combining Bounded Model Checking and Code Contracts. Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 6, pp. 22-35. http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a1/

[1] E. Clarke, D. Kroening, F. Lerda, “A Tool for Checking ANSI-C Programs”, TACAS '04, Springer-Verlag, 2004, 168–176 | Zbl

[2] A. Armando, J. Mantovani, L. Platania, “Bounded Model Checking of Software using SMT Solvers instead of SAT Solvers”, Int. J. Softw. Tools Technol. Transf., 11:1 (2009), 69–83 | DOI | MR

[3] L. Cordeiro, B. Fischer, J. Marques-Silva, “SMT-Based Bounded Model Checking for Embedded ANSI-C Software”, ASE '09, IEEE, 2009, 137–148

[4] F. Merz, S. Falke, C. Sinz, “LLBMC: Bounded Model Checking of C and C++ Programs using a Compiler IR”, VSTTE '12, Springer-Verlag, 2012, 146–161

[5] Itsykson V., Glukhikh M., “Yazyk specifikaciy povedeniya programmnyh komponentov”, Nauchno-tehnicheskie vedomosti SPbGPU. Informatika. Telekommunikacii. Upravlenie, 3 (2010), 63–71 (in Russian)

[6] V. Itsykson, A. Zozulya, “Automated Program Transformation for Migration to New Libraries”, SECR '11, IEEE, 2011, 1–7

[7] P. Baudin, J. C. Filliâtre, T. Hubert, C. Marché, B. Monate, Y. Moy, V. Prevosto, ACSL: ANSI/ISO C Specification Language. Preliminary Design, Version 1.4, , 2008 http://www.frama-c.cea.fr/download/acsl_1.4.pdf

[8] O. Sery, G. Fedyukovich, N. Sharygina, “Interpolation-Based Function Summaries in Bounded Model Checking”, HVC '11, Springer-Verlag, 2011, 160–175

[9] A. Biere, A. Cimatti, E. M. Clarke, Y. Zhu, “Symbolic Model Checking without BDDs”, TACAS '99, Springer-Verlag, 1999, 193–207

[10] C. Barrett, R. Sebastiani, S. A. Seshia, C. Tinelli, “Satisfiability Modulo Theories Handbook of Satisfiability”, Frontiers in Artificial Intelligence and Applications, 185, 2009, 825–885

[11] C. Lattner, V. Adve, “LLVM: A Compilation Framework for Lifelong Program Analysis Transformation”, CGO '04, IEEE, 2004, 75–86

[12] R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, F. K. Zadeck, “Efficiently Computing Static Single Assignment Form and the Control Dependence Graph”, ACM TOPLAS, 13:4 (1991), 451–490 | DOI

[13] K. L. McMillan, “Applications of Craig Interpolants in Model Checking”, TACAS '05, Springer-Verlag, 2005, 1–12 | Zbl

[14] W. Craig, “Three Uses of the Herbrand-Gentzen Theorem in Relating Model Theory and Proof Theory”, The Journal of Symbolic Logic, 22:3 (1957), 269–285 | DOI | MR | Zbl

[15] L. De Moura, N. Bjørner, “Z3: An Efficient SMT Solver”, TACAS '08, Springer-Verlag, 2008, 337–340

[16] C. Barrett, L. De Moura, A. Stump, “SMT-COMP: Satisfiability Modulo Theories Competition”, CAV '05, Springer-Verlag, 2005, 503–516

[17] D. R. Cok, A. Griggio, R. Bruttomesso, The 2012 SMT Competition, 2012 http://smtcomp.sourceforge.net/2012/

[18] Open Source Report 2011, , Coverity http://www.coverity.com/library/pdf/coverity-scan-2011-open-source-integrity-report.pdf

[19] NECLA Static Analysis Benchmarks, , NEC Laboratories, 2013 http://www.nec-labs.com/research/system/systems_SAV-website/benchmarks.php