Geodesic
The use of dependencies for improving the precision of program static analysis
Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 68-79.

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

The development of dependency analysis methods in order to improve static code analysis precision is considered in this paper. Reasons for precision loss is abstract interpretation methods when detecting defects in program source code are explained. The need for program object dependency extraction and interpretation is justified by numerous real-world examples. A dependency classification is presented. The necessity for aggregate analysis of values and dependencies is considered. The dependency extraction from assignment statements is described. The dependency interpretation based on logic inference using logic and arithmetic rules is proposed. The methods proposed are implemented in defect detection tool Digitek Aegis and significant increase of precision is shown.
Keywords: static analysis, abstract interpretation, dependency analysis, program defect detection. 
@article{MAIS_2011_18_4_a6,
     author = {M. I. Glukhikh and V. M. Itsykson and V. A. Tsesko},
     title = {The use of dependencies for improving the precision of program static analysis},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {68--79},
     publisher = {mathdoc},
     volume = {18},
     number = {4},
     year = {2011},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a6/}
}
TY  - JOUR
AU  - M. I. Glukhikh
AU  - V. M. Itsykson
AU  - V. A. Tsesko
TI  - The use of dependencies for improving the precision of program static analysis
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2011
SP  - 68
EP  - 79
VL  - 18
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a6/
LA  - ru
ID  - MAIS_2011_18_4_a6
ER  - 
%0 Journal Article
%A M. I. Glukhikh
%A V. M. Itsykson
%A V. A. Tsesko
%T The use of dependencies for improving the precision of program static analysis
%J Modelirovanie i analiz informacionnyh sistem
%D 2011
%P 68-79
%V 18
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a6/
%G ru
%F MAIS_2011_18_4_a6
M. I. Glukhikh; V. M. Itsykson; V. A. Tsesko. The use of dependencies for improving the precision of program static analysis. Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 68-79. http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a6/

[1] M. Zhivich, R. Cunningham, “The Real Cost of Software Errors. IEEE Security Privacy”, IEEE Computer Society, 7:2 (2009)

[2] F. Nielson, N. Nielson, C. Hankin, Principles of Program Analysis, XXI, Corr. 2nd printing, Springer, 2005, 452 pp.

[3] P. Cousot, “Abstract Interpretation. ACM Computing Surveys (CSUR)”, ACM, 28:2 (1996), 324–328

[4] N. Jones, F. Nielson, “Abstract Interpretation: A Semantic-based Tool for Program Analysis”, Handbook of logic in computer science: semantic modeling, v. 4, Oxford University Press, Oxford, 1995, 527–636 | MR

[5] V. S. Nesov, O. R. Malikov, “Ispolzovanie informatsii o lineinykh zavisimostyakh dlya obnaruzheniya uyazvimostei v iskhodnom kode programm”, Trudy ISP RAN, 2006, no. 9, 51–57

[6] P. Cousot, N. Halbwachs, “Automatic discovery of linear restraints among variables of a program”, Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '78), ACM, 1978, 84–96

[7] (Code Analysis for C/C++ Overview, Microsoft Corporation) http://msdn.microsoft.com/en-us/library/d3bbz7tz.aspx

[8] (Frama-C Software Analyzers) http://frama-c.com

[9] (Splint home page) http://www.splint.org

[10] (Fortify Software) http://www.fortify.com

[11] V. M. Itsykson, M. Yu. Moiseev, V. A. Tsesko, A. V. Karpenko, “Issledovanie sistem avtomatizatsii obnaruzheniya defektov v iskhodnom kode programmnogo obespecheniya”, Nauchno-tekhnicheskie vedomosti SPbGPU. Informatika. Telekommunikatsii. Upravlenie, 2008, no. 5(65), 119–127

[12] M. Schwartzbach, Lecture Notes on Static Analysis, Aarhus, 2000, 58 pp.

[13] V. M. Itsykson, M. Yu. Moiseev, V. A. Tsesko, A. V. Zakharov, M. Kh. Akhin, “Algoritm intervalnogo analiza dlya obnaruzheniya defektov v iskhodnom kode programm”, Informatsionnye i upravlyayuschie sistemy, 2009, no. 2(39), 34–41

[14] V. M. Itsykson, M. Yu. Moiseev, M. Kh. Akhin, A. V. Zakharov, V. A. Tsesko, “Algoritmy analiza ukazatelei dlya obnaruzheniya defektov v iskhodnom kode”, Sistemnoe programmirovanie, 2009, 5–30

[15] W. Bush, J. Pincus, D. Sielaff, “A static analyzer for finding dynamic programming errors”, Software: Practice and Experience, 30:7 (June 2000), 775–802 | 3.0.CO;2-H class='badge bg-secondary rounded-pill ref-badge extid-badge'>DOI | Zbl

[16] A. Wang, H. Fei, M. Gu, X. Song, “Verifying Java Programs By Theorem Prover HOL”, Proceedings of the 30th Annual International Computer Software and Applications Conference, IEEE Computer Society Washington DC, 01, 2006, 139–142

[17] (HOL 4 Kananaskis 6) http://hol.sourceforge.net

[18] (WHY — a software verification platform) http://why.lri.fr

[19] B. Steensgaard, “Points-to analysis in almost linear time”, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, New York, USA, 1996, 32–41 | DOI

[20] D. Avots , M. Dalton, V. Livshits, M. Lam, “Improving software security with a C pointer analysis”, Proceedings of the 27th international conference on Software engineering, New York, USA, 2005, 332–341

[21] (VCC) http://vcc.codeplex.com

[22] (Z3) http://research.microsoft.com/en-us/um/redmond/projects/z3

[23] (SMT-LIB) http://www.smtlib.org

[24] (Aegis—a defect detection system) http://www.digiteklabs.ru/aegis