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/