Fast and Safe Concrete Code Execution for Reinforcing Static Analysis and Verification
https://doi.org/10.18255/1818-1015-2015-6-763-772
Abstract
The problem of improving precision of static analysis and verification techniques for C is hard due to simplification assumptions these techniques make about the code model. We present a novel approach to improving precision by executing the code model in a controlled environment that captures program errors and contract violations in a memory and time efficient way. We implemented this approach as an executor module Tassadar as a part of bounded model checker Borealis. We tested Tassadar on two test sets, showing that its impact on performance of Borealis is minimal.
The article is published in the authors’ wording.
About the Authors
M. Belyaev
Peter the Great St. Petersburg Polytechnic University
Russian Federation
Russian Federation
assistant, Polytechnicheskaya street, 21, Saint-Petersburg, 194021
V. Itsykson
Peter the Great St. Petersburg Polytechnic University
Russian Federation
PhD, Polytechnicheskaya street, 21, Saint-Petersburg, 194021
Russian Federation
PhD, Polytechnicheskaya street, 21, Saint-Petersburg, 194021
References
1. M. Akhin, M. Belyaev, V. Itsykson, “Software defect detection by combining bounded model checking and approximations of functions”, Automatic Control and Computer Sciences, 48:7 (2014), 389–397.
2. P. Baudin, J. C. Filliˆatre, T. Hubert, C. March´e, B. Monate, Y. Moy, V. Prevosto, 2008, ACSL: ANSI/ISO C Specification Language. Preliminary Design, version 1.4., Preliminary.
3. J. L. Bentley, “Solutions to klee’s rectangle problems”, Technical report, 1977.
4. D. Beyer, “Competition on software verification”, 2012, 504–524.
5. A. Biere, A. Cimatti, E. M. Clarke, Y. Zhu, “Symbolic model checking without BDDs”, 1999, 193–207.
6. M. K. Buckland, F. C. Gey, “The relationship between recall and precision”, JASIS, 45:1 (1994), 12–19.
7. E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, “Counterexample-guided abstraction refinement”, CAV, 2000, 154–169.
8. 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.
9. A. Groce, R. Joshi, “Extending model checking with dynamic analysis”, Verification, model checking, and abstract interpretation, 2008, 142–156.
10. ISO, The ANSI C standard (C99), ISO/IEC, 1999.
11. F. Ivanˇci´c, S. Sankaranarayanan, “NECLA static analysis benchmarks”, 2009.
12. D. Kroening, A. Groce, E. Clarke, “Counterexample guided abstraction refinement via program execution”, Formal methods and software engineering, 2004, 224–238.
13. C. Lattner, V. Adve, “LLVM: A compilation framework for lifelong program analysis & transformation”, 2004, 75–86.
14. D. Novillo, “Tree SSA: A new optimization infrastructure for GCC”, Proceedings of the 2003 gCC developers’ summit, 21, 2014, 83–93.
Review
For citations:
Belyaev M., Itsykson V. Fast and Safe Concrete Code Execution for Reinforcing Static Analysis and Verification. Modeling and Analysis of Information Systems. 2015;22(6):763-772. https://doi.org/10.18255/1818-1015-2015-6-763-772
Views:
1353
Email this article 