SharpChecker: Static analysis tool for C# programsстатья
Информация о цитировании статьи получена из
Web of Science ,
Scopus
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 7 сентября 2017 г.
Авторы:
Koshelev V.K. ,
Ignatiev V.N. ,
Borzilov A.I. ,
Belevantsev A.A.
Журнал:
Programming and Computer Software
Том:
43
Номер:
4
Год издания:
2017
Издательство:
Pleiades Publishing, Ltd
Местоположение издательства:
Road Town, United Kingdom
Первая страница:
268
Последняя страница:
276
DOI:
10.1134/S0361768817040041
Аннотация:
This paper considers various aspects of static analysis of C# programs in order to detect the maximum number of software bugs in an acceptable time. A complete cycle of software static analysis is described with the main focus being placed on the specifics of the C# language. Some methods are discussed that take into account popular features of C# at all levels of analysis: call graph and control flow graph construction, dataflow analysis, as well as context- and path-sensitive interprocedural analysis. A symbolic execution method is proposed, which is based on the works devoted to the Bounded Model Checking (BMC) and the Saturn Software Analysis Project. A memory model is described that enables an accurate intraprocedural analysis and allows one to create compact representations of error conditions associated with functions, which are essential for interprocedural analysis. A special attention is paid to the optimizations that occur during path-sensitive analysis of error conditions. The conditions need to be optimized in terms of size, because path-sensitive interprocedural analysis requires saving a large number of conditions for each analyzed function. The conditions are resolved using advanced SMT solvers (such as the Microsoft Z3 Prover). This paper also considers various approaches to modeling the behavior of library functions: based on a summary containing a set of properties required for analysis, or based on simplified implementations in C#. All the discussed solutions are implemented in the SharpChecker static analysis tool and are tested on a number of open-source projects from 1.5 thousand to 1.35 million lines of code.
Original Russian Text © V.K. Koshelev, V.N. Ignatiev, A.I. Borzilov, A.A. Belevantsev, 2017, Trudy Instituta Sistemnogo Programmirovaniya, 2016, vol. 28, no 1, pp. 21–40.
Добавил в систему:
Корныхин Евгений Валерьевич