Geodesic
Fast and safe concrete code execution for~reinforcing static analysis and verification
Modelirovanie i analiz informacionnyh sistem, Tome 22 (2015) no. 6, pp. 763-772.

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

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.
Keywords: concrete interpretation, symbolic execution, static code analysis, analysis precision. 
@article{MAIS_2015_22_6_a2,
     author = {M. Belyaev and V. Itsykson},
     title = {Fast and safe concrete code execution for~reinforcing static analysis and verification},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {763--772},
     publisher = {mathdoc},
     volume = {22},
     number = {6},
     year = {2015},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a2/}
}
TY  - JOUR
AU  - M. Belyaev
AU  - V. Itsykson
TI  - Fast and safe concrete code execution for~reinforcing static analysis and verification
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2015
SP  - 763
EP  - 772
VL  - 22
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a2/
LA  - en
ID  - MAIS_2015_22_6_a2
ER  - 
%0 Journal Article
%A M. Belyaev
%A V. Itsykson
%T Fast and safe concrete code execution for~reinforcing static analysis and verification
%J Modelirovanie i analiz informacionnyh sistem
%D 2015
%P 763-772
%V 22
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a2/
%G en
%F MAIS_2015_22_6_a2
M. Belyaev; V. Itsykson. Fast and safe concrete code execution for~reinforcing static analysis and verification. Modelirovanie i analiz informacionnyh sistem, Tome 22 (2015) no. 6, pp. 763-772. http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a2/

[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 | DOI

[2] 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., Preliminary, 2008

[3] J. L. Bentley, Solutions to klee's rectangle problems, Technical report, Carnegie-Mellon Univ., Pittsburgh, PA, 1977

[4] D. Beyer, Competition on software verification, Springer, 2012, 504–524 | Zbl

[5] A. Biere, A. Cimatti, E. M. Clarke, Y. Zhu, “Symbolic model checking without BDDs”, Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, 1579, 1999, 193–207 | DOI

[6] M. K. Buckland, F. C. Gey, “The relationship between recall and precision”, JASIS, 45:1 (1994), 12–19 | 3.0.CO;2-L class='badge bg-secondary rounded-pill ref-badge extid-badge'>DOI

[7] E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, “Counterexample-guided abstraction refinement”, CAV, 2000, 154–169 | Zbl

[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 | DOI

[9] A. Groce, R. Joshi, “Extending model checking with dynamic analysis”, Verification, model checking, and abstract interpretation, 2008, 142–156 | DOI | Zbl

[10] The ANSI C standard (C99), ISO/IEC, 1999

[11] F. Ivančić, 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, Springer, 2004, 224–238 | DOI

[13] C. Lattner, V. Adve, “LLVM: A compilation framework for lifelong program analysis transformation”, Proceedings of the 2004 International Symposium on Code Generation and Optimization, CGO'04 (Palo Alto, California, Mar. 2004), 75–86

[14] D. Novillo, “Tree SSA: A new optimization infrastructure for GCC”, Proceedings of the 2003 gCC developers' summit, 2003, 181–193