Proceedings of the Institute for System Programming of the RAS
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Proceedings of ISP RAS:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Proceedings of the Institute for System Programming of the RAS, 2016, Volume 28, Issue 1, Pages 21–40
DOI: https://doi.org/10.15514/ISPRAS-2016-28(1)-2
(Mi tisp2)
 

This article is cited in 7 scientific papers (total in 7 papers)

C# static analysis framework

V. K. Koshelev, V. N. Ignatyev, A. I. Borzilov

ISP RAS, 25 Alexander Solzhenitsyn Str., Moscow, 109004, Russian Federation
Full-text PDF (411 kB) Citations (7)
References:
Abstract: The paper describes static analysis techniques that are used for defect detection in C# programs. The goal of proposed analysis approaches is to catch more defects within an acceptable amount of time. Although the paper contains a description of full analysis cycle, it mainly focuses on special aspects that distinguish C# analysis approaches from well-known Java and C++ techniques. The paper illustrates methods that allow taking into account C# specialties of all analysis stages: call graph and control flow graph construction, data flow analysis, context- and path-sensitive interprocedural analysis. We propose an adaptation of symbolic execution methods inspired by Bounded Model Checking and Saturn Software Analysis Project. The paper also explains the organization of memory model, which is suitable for both a precise intraprocedural analysis and a creation of compact function-bound conditions used for interprocedural analysis. Special attention is paid to optimization of condition size and simplicity during a path sensitive-analysis. The conditions produced by a path-sensitive analysis are supposed to be solved by modern SMT solvers like Microsoft Z3 Prover. Different approaches to external functions modeling are covered. All proposed approaches are implemented in the SharpChecker static analysis tool and, as evaluated on several open source C# projects of varying size (1K - 1.35M lines of code), display good results and scalability.
Keywords: Roslyn, C#, static analysis, null pointer dereference, path-sensitive analysis, context-sensitive analysis, function summary, bug detection.
Bibliographic databases:
Document Type: Article
Language: Russian
Citation: V. K. Koshelev, V. N. Ignatyev, A. I. Borzilov, “C# static analysis framework”, Proceedings of ISP RAS, 28:1 (2016), 21–40
Citation in format AMSBIB
\Bibitem{KosIgnBor16}
\by V.~K.~Koshelev, V.~N.~Ignatyev, A.~I.~Borzilov
\paper C\# static analysis framework
\jour Proceedings of ISP RAS
\yr 2016
\vol 28
\issue 1
\pages 21--40
\mathnet{http://mi.mathnet.ru/tisp2}
\crossref{https://doi.org/10.15514/ISPRAS-2016-28(1)-2}
\elib{https://elibrary.ru/item.asp?id=26166300}
Linking options:
  • https://www.mathnet.ru/eng/tisp2
  • https://www.mathnet.ru/eng/tisp/v28/i1/p21
  • This publication is cited in the following 7 articles:
    Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Proceedings of the Institute for System Programming of the RAS
     
      Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024