Geodesic
LLVM-based static analysis tool using type and effect systems
Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 45-55.

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

The intention of this paper is to describe a static analysis tool under development. The principal idea behind the design of this tool is to use type and effect systems for static analysis of real programs. The tool uses LLVM bitcode files as input, thus extending the set of analyzed languages to those supported by LLVM compiler infrastructure. It uses its own parser of bitcode files and a program model similar to that of LLVM. The approach taken is to research feasibility of designing instruments for static analysis by applying known type and effect system based algorithms for detecting defects to LLVM bitcode language and effectively to the original source code.
Keywords: static program analysis, type and effect system, low level virtual machine, defect detection
Mots-clés : SSA. 
@article{MAIS_2011_18_4_a4,
     author = {M. A. Belyaev and V. A. Tsesko},
     title = {LLVM-based static analysis tool using type and effect systems},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {45--55},
     publisher = {mathdoc},
     volume = {18},
     number = {4},
     year = {2011},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a4/}
}
TY  - JOUR
AU  - M. A. Belyaev
AU  - V. A. Tsesko
TI  - LLVM-based static analysis tool using type and effect systems
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2011
SP  - 45
EP  - 55
VL  - 18
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a4/
LA  - ru
ID  - MAIS_2011_18_4_a4
ER  - 
%0 Journal Article
%A M. A. Belyaev
%A V. A. Tsesko
%T LLVM-based static analysis tool using type and effect systems
%J Modelirovanie i analiz informacionnyh sistem
%D 2011
%P 45-55
%V 18
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a4/
%G ru
%F MAIS_2011_18_4_a4
M. A. Belyaev; V. A. Tsesko. LLVM-based static analysis tool using type and effect systems. Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 45-55. http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a4/

[1] Coverity Scan Open Source Report, 2009 http://scan.coverity.com/report/

[2] M. A. Ertl, “Wien TU: Domination-Based Scoping and Static Single Assignment Languages”, Static Single-Assignment Form Seminar, 2009 | Zbl

[3] S. Horwitz, “Precise Flow-Insensitive May-Alias Analysis is NP-Hard”, ACM Transactions on Programming Languages and Systems, 1997, ACM Association for Computing Machinery, 1–6 | DOI | Zbl

[4] V. Itsykson, M. Moiseev, V. Tsesko, A. Zakharov, “Automatic defects detection in industrial C/C++ software”, Software Engineering Conference in Russia (CEE-SECR), 2009 | Zbl

[5] T. Jim, J. Palsberg, Type inference in systems of recursive types with subtyping, Manuscript, 1999

[6] C. Lattner, J. Haberman, P. S. Housel, LLVM Bitcode File Format http://llvm.org/docs/BitCodeFormat.html

[7] C. Lattner, LLVM Language Reference Manual http://llvm.org/docs/LangRef.html

[8] A haskell library for parsing LLVM binary bitcode files (llvm-parser) http://code.google.com/p/llvm-parser

[9] D. Marino, T. Millstein, A Generic Type-and-Effect System. TLDI, 2010

[10] F. Nielson, H. R. Nielson, “Type and Effect Systems”, Correct System Design, 1999, 114–136 | DOI

[11] F. Nielson, H. R. Nielson, C. Hankin, Principles of Program Analysis, Springer-Verlag, 2005

[12] K. P. D. Ross, “From System F to Typed Assembly Language”, Twenty-Fifth ACM SIGPLAN Symposium on Principles of Programming Languages, 1998, 85–97

[13] K. Zadeck, “The Development of Static Single Assignment Form”, Static Single-Assignment Form Seminar, 2009