ReferencesMarat Akhin, Mikhail Belyaev, Vladimir Itsykson“Defect Detection: Combining Bounded Model Checking and Code Contracts”, Model. Anal. Inform. Sist., 2013, Volume 20, Number 6,Pages 22

Defect Detection: Combining Bounded Model Checking and Code Contracts
Marat Akhin, Mikhail Belyaev, Vladimir Itsykson



References

1.	E. Clarke, D. Kroening, F. Lerda, “A Tool for Checking ANSI-C Programs”, TACAS '04, Springer-Verlag, 2004, 168–176
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
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. Filliâtre, T. Hubert, C. Marché, B. Monate, Y. Moy, V. Prevosto, ACSL: ANSI/ISO C Specification Language. Preliminary Design, Version 1.4, http://www.frama-c.cea.fr/download/acsl_1.4.pdf, 2008
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
13.	K. L. McMillan, “Applications of Craig Interpolants in Model Checking”, TACAS '05, Springer-Verlag, 2005, 1–12
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
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, http://www.coverity.com/library/pdf/coverity-scan-2011-open-source-integrity-report.pdf, Coverity
19.	NECLA Static Analysis Benchmarks, http://www.nec-labs.com/research/system/systems_SAV-website/benchmarks.php, NEC Laboratories, 2013