Введение 7
Глава 1. Обзор литературы 14
1.1 Анализаторы кода 14
1.2 Представление структуры программного кода 17
1.3 Языки спецификации поведения 20
1.4 Методы верификации 21
1.5 Методы интеграции 24
Глава 2. Архитектура программного решения 26
Глава 3. Особенности чтения исходных текстов 27
3.1 Формальная модель программы 27
3.2 Семантики языков программирования 29
3.3 Организация языково-независимого чтения 30
3.4 Метод чтения нескольких файлов и объединения их семантики34
3.5 Система типов данных 37
3.5.1 Принципы хранения данных 38
3.5.2 Структура типов 41
3.6 Организация чтения и записи сериализированных данных . . 42
Глава 4. Виртуальная машина и промежуточное представление Midair 44
4.1 Язык Midair 44
4.2 Гипервизор и виртуальные машины 45
4.3 Трансляция подпрограмм из обобщенных деревьев в
промежуточное представление 46
4.3.1 Метод обобщения 50
4.3.2 Метод инстанцирования 52
4.4 Модифицирование и упрощение команд в результате анализа .53
4.5 Поддержка различных языков программирования в одном
контексте 54
Глава 5. Структура и функции гибридного решателя 56
5.1 Аналитическое представление программы 56
5.2 Моделирование памяти 57
5.2.1 Версионирование переменных 58
5.2.2 Разбиение на регионы 60
5.2.3 Анализ псевдонимов 62
5.2.4 Инкрементальные и кумулятивные модели 65
5.2.5 Свойства и их перенос 66
5.3 Метод трансформации программ в SMT-представление ....68
5.4 Обнаружение ошибок при помощи SMT-решателя 72
5.5 Обнаружение ошибок с помощью вычислителя 73
5.6 Ошибки типов 75
Глава 6. Интеграции с языковыми инструментами 77
6.1 Контракты в языке РуСи 77
6.2 Проверка комментариев Doxygen 78
6.3 Анализ групп связности 79
6.4 Анализ зависимостей 80
6.5 Анализ языка 81
6.6 Композиционный анализ 82
6.7 Интерфейс клиент-серверного взаимодействия 83
6.8 Интерактивное управление 83
6.9 Интеграция различных архитектур и компиляторов 84
6.10 Моделирование поддержки различных операционных систем .88
6.11 Сканирующий запуск компиляции 89
6.12 Эмуляция окружения на основе аргументов компиляторов . .90
Глава 7. Обеспечение качества решения 92
7.1 Тестирование в различных режимах и средах 93
Глава 8. Апробация решения 95
8.1 Апробация в синтетических тестах 95
8.2 Апробация на промышленных проектах 96
8.3 Тестирование межъязыкового анализа 97
8.4 Тестирование технологического решения по интеграции ...99
8.5 Апробация в научном сообществе 101
Заключение 103
Словарь терминов 105
Список литературы 109
Приложение А. Схема работы анализатора 128
Приложение Б. Поддерживаемые дополнения 129
Приложение В. Обнаруживаемые классы ошибок 130
Приложение Г. Схема работы модуля чтения 131
Приложение Д. Универсальный языковой базис 132
Приложение Е. Принцип работы подсистемы виртуальных машин134
Приложение Ж. Команды языка Midair 135
Приложение З. Типы и их размеры 138
Приложение И. Отображение конструкций C++ в языковой базис .139
Приложение К. Отображение конструкций РуСи в языковой базис143
Приложение Л. Отображение конструкций ACSL в языковой базис145
Приложение М. Перенос тегов между регионами памяти 147
Приложение Н. Уникальные конструкции языков 148
Приложение О. Основные группы юнит-тестов 149
Приложение П. Организация системного тестирования 150
Стр.
Приложение Р. Организация тестирования в различных средах . .151
Приложение С. Результат тестирования на бенчмарке Toyota ITC .152
Стремительное развитие микроэлектроники в 20 веке привело к распространению кремниевых микросхем в различных сферах человеческой деятельности. Долгое время увеличение производительности процессоров происходило через увеличение числа транзисторов по закону Мура [1], но индустрия постепенно стала подходить к физическим пределам плотности их размещения, что потребовало новых подходов к производству транзисторов [2]. Индустрия ответила концепцией параллельных вычислений, появились спекулятивное исполнение, внеочередное исполнение и другие технологии, повышающие производительность. Появились специализированные микросхемы, которые добились большей производительности благодаря специализации вычислений. Первыми такими микросхемами стали видео-ускорители. В дальнейшем стали развиваться программируемые микросхемы (FPGA) [3; 4], сетевые процессоры, нейросетевые процессоры, акселераторы глубокого обучения [5], сопроцессоры.
Такие методы решения проблемы производительности привели к значительному увеличению сложности разработки программного обеспечения. Программное обеспечение теперь одновременно разрабатывается для компьютеров, внешних устройств, сопроцессоров, FPGA, требует обучения сопутствующих нейронных сетей. В начале века на рынке процессоров господствовала архитектура x86, и разработчики предпочитали писать программы только под нее. Остальные архитектуры не были массовыми. В настоящее время самой популярной архитектурой можно считать ARM [6] в связи с выпуском большого количества устройств на базе Android [7] (на базе Linux), для стационарных компьютеров — x86_64 (amd64) [8], для маршрутизаторов — MIPS. Переход компании Apple на архитектуру Apple Silicon [9] — процессоров M1 на базе ARM — существенно изменил отношение рынка к процессорам ARM, и теперь сложно представить современную программу для массового потребителя без поддержки данной архитектуры.
Эта тенденция прямо влияет на анализ программ с целью выявления ошибок и несоответствия спецификации. Ранние программы для ЭВМ можно было формально доказать с первой до последней строки в связи с их небольшим размером, но современные программы состоят из множества модулей, в том числе внешних, написанных на разных языках, для множества операционных систем и для различающегося аппаратного обеспечения. В качестве примера можно привести современные системы быстрого оптического распознавания: низкоуровневое программное обеспечение для камеры и другой периферии написано на С или ассемблере (архитектура может быть различной), прошивка микроконтроллера, использующего камеру, написана на C/C++ (чаще всего для архитектуры ARM), передача потока осуществляется на сервер на базе архитектуры AMD64, нейронная сеть тренируется на нейросетевом процессоре, используются FPGA для увеличения производительности, вывод осуществляется при помощи графического ускорителя. Проверить алгоритмы таких программ очень сложно.
Разнообразие конфигураций порождает проблемы совместимости и масштабируемости. Возникает вопрос: как производить качественный статический анализ программ на разных языках, для разных процессоров, операционных систем?
После значительного числа инцидентов [10;11], связанных с ошибками в программах, исследователи разработали методы защиты от ошибок. Их можно разбить на несколько групп:
- Установка требований к программному коду, ограничение используемых конструкций. Организации могут запретить использовать арифметику указателей в C [12], являющуюся значительным источником ошибок. Однако данный метод является организационным, т.к. он не предотвращает возможность допустить ошибку, а скорее делает её затруднительной.
- Защитные языки программирования. Их идея сводится к снижению возможности допустить ошибку — в основном, за счет удачного синтаксиса и проверок в компиляторе [13]. Интересным способом достижения корректности является использование сертифицированных компиляторов, таких как CompCert [14].
- Анализ программ — это проверка программного кода. Он может осуществляться как статически, т.е. без запуска программы и с учетом всех возможных путей исполнения, так и динамически, т.е. с запуском программы и с учетом только действующих путей исполнения. Статические проверки кода могут проводиться через проверку модели, т.е. сравнение реальной программы с эталоном, заданным либо полностью формальной моделью, либо через аннотации. Другой вариант — через символьное исполнение программы, которое не исключает возможность последующей проверки модели.
- Методы предотвращения ошибок на уровне среды исполнения. Один из наиболее очевидных способов — запрет обращения к определенной памяти через проверку допустимости действия во время исполнения, явный запрет разыменования нулевых указателей и т.п.
Комбинирование указанных методов является эффективным способом достижения безопасности программ [15], что подтверждается их использованием в авионике [16] и других сферах, где качество кода критически важно.
Несмотря на разнообразие подходов, в настоящий момент в сфере разработки безопасного программного обеспечения наблюдается некоторая стагнация. Крупные организации все чаще предлагают разработчикам пере-ходить на новые «безопасные» языки программирования, такие как Rust [17], Go [18], а также интерпретируемые языки с JIT [19]: C# [20], Kotlin [21]. Обсуждается даже добавление модулей на языке Rust в Linux [22]. Несмотря на все достоинства безопасных языков, перенос кодовой базы на них является крайне амбициозной задачей. Вероятен сценарий, когда новые ошибки будут добавлены просто вследствие переписывания достаточно хорошо протестированной (но ни в коем случае не безошибочной) кодовой базы на новый язык.
Другая проблема заключается в том, что расширение количества поддерживаемых программным проектом языковых семантик неизбежно влечет необходимость контроля за всеми реализаций как по отдельности, так и в совокупности, что не может не снизить качество программы. При этом статический анализ зачастую достаточно прогрессивен технически, чтобы поддерживать разные языки, но межъязыковое взаимодействие остается нерешенной проблемой. Многоязыковые анализаторы обычно имеют возможность переходить границы языков в рамках одной технологии (JVM [23], .NET [24], биткоды LLVM [25]), но не далее.
Немаловажным является и опыт разработчиков. Переход с одного языка на другой оправдан, если это в небольшой степени влияет на накопленный программистами опыт, не «обнуляет» его. Например, переход с Java на Kotlin не влияет на опыт, если программа пишется в стиле Java, но Kotlin добавляет функциональные вставки, корутины и другие возможности, использование которых рекомендуется разработчиками языка. При этом «бесшовность» перехода в таком случае является весьма относительной с точки зрения опыта программистов.
Таким образом, переход на безопасные языки программирования является устойчивой тенденцией, при этом процесс происходит медленно: разработчикам и их инструментам необходимо поддерживать взаимодействующие кодовые базы на разных языках.
К настоящему моменту статические анализаторы кода сформировались в отдельные программные продукты, которые обеспечивают две основные сервисные модели: локальную проверку кода и работу на сервере в рамках Continuous Integration.Фактическое отсутствие других моделей существенно ограничивает взаимодействие анализаторов с внешними программами. Если сделать анализатор менее зависимым от модели использования, то из анализа можно извлечь больше полезных сведений: дополнительные статические инварианты, данные для генерации юнит-тестов, сведения для поддержки межъязыковых контрактов, пути исполнения программ и т.п.
В работе [26] автор рассматривает возможность применения статических анализаторов в рамках нетрадиционных сервисных моделей. Это требует корректировки принципа работы самого анализатора.
Подобные модели требуются для комплексной среды программирования [27;28], разрабатываемой на кафедре системного программирования Санкт-Петербургского государственного университета под руководством заведующего кафедрой, профессора Андрея Николаевича Терехова. Проект ставит перед собой амбициозную задачу разработки комплексной технологии программирования, подразумевающей полный цикл: языки программирования, компиляторы [29], статические и динамические анализаторы, методы оптимизации программ, виртуальные машины для исполнения [30], кодизайн аппаратного обеспечения [31], тестирование. Важное свойство проекта — взаимодействие с другими языками программирования.
Перед статическими анализаторами в комплексных средах стоит множество вызовов. Во-первых, велика зависимость инструментов анализа от систем чтения кода и их внутренних структур данных. Во-вторых, у анализаторов зачастую отсутствует точная информация о целевой платформе. В-третьих, анализаторы часто не приспособлены к анализу на стадии проектирования, не подразумевают интерактивности и неклассических моделей использования. В-четвертых, реализация независимых инструментов в таких условиях неминуемо становится сложной.
Таким образом, комплексные среды разработки предполагают, что анализаторы имеют гибридность (поддержку различных методов анализа от контроля синтаксических деревьев до проверки модели, абстрактной интерпретации), языковую независимость (работоспособность на про-граммах, написанных на разных языках программирования, возможность их анализа в одном контексте), поддержку различных программно-аппаратных платформ с адаптацией (маскировкой) под наборы компиляции для уточнения данных о целевой платформе, простоту интеграции во весь цикл разработки от проектирования до тестирования и итогового приема, широкую функциональность (обнаружение дефектов, проверки инвариантов, определение языка проекта, описание существующих в коде переменных, функций и их назначения, навигация по коду, выявление параметров сложности кода, определение зависимостей, помощь в сертификации). Анализаторам необходимо не только соответствовать всем этим требованиям, но и обеспечивать идентичный опыт разработки на различных технологиях. По отдельности эти задачи решаются, но комплексный подход к созданию данной «экосистемы» по существу не рассматривался и является актуальной задачей программной инженерии.
Для создания подходящего под эти требования статического анализатора необходимо техническое решение, обладающее широким спектром возможностей. Equid [32] разрабатывается автором с 2015 г. Проект развился из обычного анализатора шаблонов в анализатор путей исполнения для поиска состояний гонки [33], а затем был развит до полнофункционального анализатора [34]. Проект был успешно применен в различных коммерческих проектах и доказал свою эффективность в решении промышленных задач.
Целью данной работы является разработка методологии проведения статического анализа для комплексной технологии программирования на базе языков C, C++, РуСи с учетом требований о возможности взаимодействия различных частей программного комплекса, полноценной поддержке различных языков программирования и их применения в одном контексте.
Для достижения поставленной цели необходимо решить следующие задачи:
1. Разработать метод трансляции абстрактного синтаксического дерева в обобщенное синтаксическое дерево на основе унифицированного языкового базиса (Гл.3).
2. Подготовить алгоритм трансляции обобщенных синтаксических деревьев в промежуточное представление, обеспечивающее анализ программ на разных языках программирования. (Гл. 4).
3. Исследовать методы композиции семантик различных языков программирования и предложить вариант, позволяющий объединить в одном анализе программы на C, C++, РуСи и других потенциальных языках (п. 4.5).
4. Организовать взаимодействие между методами проверки модели, абстрактной интерпретации и символьного исполнения для проведения качественного и быстрого анализа в условиях многоязыковой среды (Гл.5)
5. Исследовать архитектуры и способы обеспечения взаимодействия статического анализатора с другими частями комплекса, реализовать библиотеки для обеспечения их бесшовного взаимодействия (Гл.6).
6. Подготовить архитектурное решение для программного продукта, поддерживающее разработанные методы во всей полноте (Гл.2).
7. Реализовать разработанные методы и интегрировать их в систему статического анализа.
Научная новизна. Новизной обладает методология обеспечения анализа «в целом», состоящая из следующих частей:
1. Методы трансляции программ в обобщенные синтаксические деревья (Гл.3) и промежуточное представление (п. 4.3).
2. Язык промежуточного представления Midair, а также соответствующий фреймворк для анализа, состоящий из виртуальных машин и гипервизоров (Гл. 4).
3. Эффективные алгоритмы гибридного решателя, подходящие для межъязыкового анализа (Гл.5).
4. Архитектура и методы обеспечения взаимодействия с компонентами комплексной технологии программирования (Гл.6).
Теоретическая и практическая значимость. Теоретический результат работы — разработанная методология проведения статического анализа, складывающаяся из сочетания алгоритмов, архитектурных и технических решений, а также опыта решений проблем, и позволяющая проводить анализ программ из разных языковых контекстов.
Практическая значимость определяется фактом разработки средства анализа кода для языков C, C++, РуСи, используемого в промышленных компаниях.
Методология и методы исследования. В работе используются базвые методы информатики и программной инженерии. Статический анализ основывается на методах проверки модели, символьного исполнения и абстрактной интерпретации. Разработанное языково-независимое представление строится на теории компиляторов. Активно используются методы теории для задачи выполнимости формул в теориях (SMT).
Личный вклад. Автор самостоятельно разработал статический анализатор и основные библиотеки для взаимодействия с ним, подготовил и описал методологический базис. Автор консультировал разработчиков дополнения поддержки статического анализа для интегрированного средства разработки комплексной технологии программирования, лично внедрил поддержку анализа в компилятор РуСи, а также вносил правки в другие элементы комплексной технологии программирования.
Основные выносимые на защиту результаты работы заключаются в следующем:
1. В рамках исследования была разработана методология проведения статического анализа для комплексной технологии программирования на базе C, C++, РуСи с учетом требования по анализу программ на этих языках в одном контексте. Это требовало создания языково-независимых методов чтения исходных текстов, промежуточного представления Midair, фреймворка виртуальных машин и гибридного решателя, поддерживающих анализ многоязычных программ на разных уровнях.
2. Сформирована методическая основа для обеспечения взаимодействия различных частей программного комплекса.
3. Автором была спроектирована архитектура анализатора, воплощающая разработанную методологию.
4. Спроектированная система была практически реализована на языках C/C++ с частичным использованием ANTLR, LLVM/Clang, CVC4/Z3 и других открытых индустриальных модулей.
5. Была произведена апробация системы, которая выявила высокое качество алгоритмов обнаружения ошибок, показала возможность применения межъязыкового анализа, а также подтвердила способности проекта по интеграции с внешними средствами комплексной среды программирования.
Рекомендуется использовать наработки данного исследования в системах статического анализа, предназначенных для комплексных сред программирования, где необходимо эффективно и единообразно анализировать программы на разных языках программирования.
В дальнейшем планируется испытать анализатор на большем числе открытых проектов, поучаствовать в различных соревнованиях по качеству анализа. В систему будут добавлены детекторы других языков программирования, увеличена точность анализа за счет применения решателей дизъюнктов Хорна. С большой долей вероятности проект будет открыт для использования внешними участниками.
В заключение автор выражает благодарность Терехову А. Н. за научное руководство, поддержку и помощь при работе над выпускной квалификационной работой. Также автор благодарит коммерческие организации, в которых он работал, за помощь в подготовке тестового материала и за поддержку на ранних этапах развития проекта. Значительный вклад в проект внесли анонимные рецензенты поданных автором на различные конференции статей, отзывы участников конференций. Отдельное спасибо супруге Светлане и дочери Софье за помощь в подготовке исследования.
1. Schaller, R. R. Moore’s law: past, present and future [Text] / R. R. Schaller // IEEE spectrum. — 1997. — Vol. 34, no. 6. — P. 52—59.
2. Shalf, J. M. Computing beyond Moore’s Law [Text] / J. M. Shalf, R. Le¬land // Computer. — 2015. — Vol. 48, no. 12. — P. 14—23.
3. Kuon, I. FPGA architecture: Survey and challenges [Text] / I. Kuon, R. Tessier, J. Rose. — Now Publishers Inc, 2008.
4. Koch, D. FPGAs for Software Programmers [Text] / D. Koch, F. Hannig, D. Ziener. — Springer International Publishing, 2016.
5. Survey of machine learning accelerators [Text] / A. Reuther [et al.] // 2020 IEEE High Performance Extreme Computing Conference (HPEC). — IEEE. 2020. — P. 1—12.
6. Singh, M. P. Evolution of processor architecture in mobile phones [Text] / M. P. Singh, M. K. Jain // International Journal of Computer Applications. —
2014. - Vol. 90, no. 4. - P. 34-39.
7. Haase, C. Androids: The Team That Built the Android Operating System [Text] / C. Haase. — Chet Haase, 2021.
8. Ledin, J. Modern Computer Architecture and Organization: Learn X86, ARM, and RISC-V Architectures and the Design of Smartphones, PCs, and Cloud Servers [Text] / J. Ledin. — Packt Publishing, 2020.
9. Apple announces Mac transition to Apple silicon [Текст]. — URL: https://www.apple.com/newsroom/2020/06/apple-announces-mac-transition-to-apple-silicon(дата обр. 30.05.2022).
10. Le Lann, G. An analysis of the Ariane 5 flight 501 failure-a system engineer-ing perspective [Text] / G. Le Lann // Proceedings International Conference and Workshop on Engineering of Computer-Based Systems. — 1997. — P. 339—346.
11. Leveson, N. An investigation of the Therac-25 accidents [Text] / N. Leve¬son, C. Turner // Computer. — 1993. — Vol. 26, no. 7. — P. 18—41.
12. Guidelines for the Use of the C Language in Critical Systems [Text] / M. T. M. I. S. R. Association [et al.]. — 2004.
13. Klabnik, S. The Rust Programming Language (Covers Rust 2018) [Text] / S. Klabnik, C. Nichols. — No Starch Press, 2019.
14. CompCert-a formally verified optimizing compiler [Text] / X. Leroy [et al.] // ERTS 2016: Embedded Real Time Software and Systems, 8th Eu¬ropean Congress. — 2016.
15. Hobbs, C. Embedded software development for safety-critical systems [Text] / C. Hobbs. — CRC Press, 2019.
16. Rierson, L. Developing safety-critical software: a practical guide for avia¬tion software and DO-178C compliance [Text] / L. Rierson. — CRC Press,
2017.
17. Blandy, J. Programming Rust: Fast, Safe Systems Development [Text] /
J. Blandy, J. Orendorff. — O’Reilly Media, 2017.
18. Martin, E. Go in Action [Text] / E. Martin, W. Kennedy, B. Ketelsen. — Manning, 2015.
19. Srikant, Y. The Compiler Design Handbook: Optimizations and Machine Code Generation, Second Edition [Text] / Y. Srikant, P. Shankar. — CRC Press, 2018.
20. Skeet, J. C# in Depth: Fourth Edition [Text] / J. Skeet. — Manning Publica-tions, 2019.
21. Jemerov, D. Kotlin in Action [Text] / D. Jemerov, S. Isakova. — Manning, 2017.
22. Gaynor, A. Linux kernel modules in rust [Text] / A. Gaynor, G. Thomas // Proceedings of the Linux Security Summit North America. — 2019. — Vol. 2019.
23. Leun, V. van der. Introduction to JVM Languages [Text] / V. van der Leun. — Packt Publishing, 2017.
24. Hewardt, M. .NET Internals and Advanced Debugging Techniques [Text] / M. Hewardt. — Addison Wesley Professional, 2014. — (Addison-wesley Microsoft Technology).
25. Lattner, C. LLVM and Clang: Next generation compiler technology [Text] / C. Lattner // The BSD conference. Vol. 5. — 2008.
26. Menshikov, M. A. Review of static analyzer service models [Текст] / M. A. Menshikov // Труды института системного программирования РАН. - 2021. — Т. 33, № 3. — С. 27 40.
27. Терехов, А. Н. Инструментальное средство обучения программированию и технике трансляции [Текст] / А. Н. Терехов // Компьютерные инструменты в образовании. — 2016. — № 1.
28. Терехов, А. Н. Проект РуСи для обучения и создания высоконадежных программных систем [Текст] / А. Н. Терехов, М. А. Терехов // Известия высших учебных заведений. Северо-Кавказский регион. Технические науки. — 2017. — 3 (195). — С. 70—75.
29. Архипов, И. С. Генерация оптимального объектного кода [Текст] / И. С. Архипов. — 2021.
30. Терехов, А. Н. Виртуальная машина для проекта РуСи [Текст] / А. Н. Терехов, А. В. Митенев, М. А. Терехов // Компьютерные инструменты в образовании. — 2016. — № 6. — С. 33—41.
31. Medvedev, O. Using hardware-software codesign language to implement CANSCID [Text] / O. Medvedev, I. Posov // Eighth ACM/IEEE In-ternational Conference on Formal Methods and Models for Codesign (MEMOCODE 2010). — 2010. — P. 85—88.
32. Menshikov, M. Equid - a static analysis framework for industrial applica¬tions [Text] / M. Menshikov // International Conference on Computational Science and Its Applications. — Springer. 2019. — P. 677—692.
33. Меньщиков, М. А. Нахождение условий гонки в коде на C методом статического анализа [Текст] / М. А. Меньщиков. — 2016.
34. Меньщиков, М. А. Гибридная система статического анализа с доказательной проверкой инвариантов [Текст] / М. А. Меньщиков. — 2018.
35. Static analyzer Svace for finding defects in a source program code [Text] / V. Ivannikov [et al.] // Programming and Computer Software. — 2014. — Vol. 40, no. 5. — P. 265—275.
36. Бородин, А. Е. Статический анализатор Svace как коллекция анализа-торов разных уровней сложности [Текст] / А. Е. Бородин, А. А. Белеванцев // Труды Института системного программирования РАН. —
2015. — Т. 27, № 6.
37. Aegis [Текст]. — URL: http : / /www. digiteklabs . ru/aegis (дата обр. 30.05.2022).
38. Akhin, M. K. Software defect detection by combining bounded model checking and approximations of functions [Text] / M. K. Akhin, M. A. Belyaev, V. M. Itsykson // Automatic Control and Computer Sci¬ences. - 2014. - Vol. 48, no. 7. - P. 389-397.
39. Akhin, M. Borealis bounded model checker: the coming of age story [Text] / M. Akhin, M. Belyaev, V. Itsykson // Present and Ulterior Software Engi-neering. — Springer, 2017. — P. 119—137.
40. PVS-Studio [Текст]. — URL: https://pvs-studio.com/ru(дата обр. 30.05.2022).
41. Menshchikov, M. 5W+1H static analysis report quality measure [Text] / M. Menshchikov, T. Lepikhin // International Conference on Tools and Methods for Program Analysis. — Springer. 2017. — P. 114—126.
42. Фадин, А. А.Appchecker - инструмент статического анализа [Текст] / А. А. Фадин, С. Борзых, П. Гусев // Control Engineering Россия. — 2017. — № 2. — С. 26—29.
43. Швед, П. Опыт развития инструмента статической верификации BLAST [Текст] / П. Швед, В. Мутилин, М. Мандрыкин // Программирование. — 2012. — Т. 38, № 3. — С. 24—35.
44. A few billion lines of code later: using static analysis to find bugs in the real world [Text] / A. Bessey [et al.] // Communications of the ACM. — 2010. — Vol. 53, no. 2. — P. 66—75.
45. cppcheck - A tool for static C/C++ code analysis [Текст]. — URL: https://cppcheck.sourceforge.io (дата обр. 30.05.2022).
46. Cppcheck Premium [Текст]. — URL: https://www.cppchecksolutions.com(дата обр. 30.05.2022).
47. Campbell, G. A. SonarQube in action [Text] / G. A. Campbell, P. P. Papa- petrou. — Manning Publications Co., 2013.
48. Semgrep [Текст]. — URL: https://semgrep.dev(дата обр. 30.05.2022).
49. QL for source code analysis [Text] / O. De Moor [et al.] // Seventh IEEE International Working Conference on Source Code Analysis and Manipu-lation (SCAM 2007). — IEEE. 2007. — P. 3—16.
50. CLion - A cross-platform IDE for C and C++ [Текст]. — URL: https://www.jetbrains.com/clion(дата обр. 30.05.2022).
51. Gqsior, L. ReSharper Essentials [Text] / E. Gqsior. — Packt Publishing, 2014. — (Community experience distilled).
52. What is clangd? [Текст]. — URL: https://clangd.llvm.org (дата обр. 30.05.2022).
53. The IntelliJ Platform: A Framework for Building Plugins and Mining Software Data [Текст] / Z. Kurbatova [и др.] // 2021 36th IEEE/ACM International Conference on Automated Software Engineering Workshops (ASEW). - 2021. - С. 14-17.
54. Schubert, P. D. Phasar: An inter-procedural static analysis framework for C/C++ [Text] / P. D. Schubert, B. Hermann, E. Bodden // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2019. — P. 393—410.
55. Vermeir, N. .NET Compiler Platform [Text] / N. Vermeir // Introducing .NET 6: Getting Started with Blazor, MAUI, Windows App SDK, Desk¬top Development, and Containers. — Berkeley, CA : Apress, 2022. — P. 275—295.
56. Bock, J. .NET Development Using the Compiler API [Text] / J. Bock. — Apress, 2016.
57. The ASTREE analyzer [Text] / P. Cousot [et al.] // European Symposium on Programming. — Springer. 2005. — P. 21—30.
58. Cousot, P Abstract interpretation [Text] / P. Cousot // ACM Computing Surveys (CSUR). - 1996. - Vol. 28, no. 2. - P. 324-328.
59. Delmas, D. Astree: From research to industry [Text] / D. Delmas, J. Souyris // International Static Analysis Symposium. — Springer. 2007. — P. 437—451.
60. Hojjat, H. The ELDARICA horn solver [Text] / H. Hojjat, P. Rummer // 2018 Formal Methods in Computer Aided Design (FMCAD). — IEEE.
2018. - P. 1-7.
61. Horn clause solvers for program verification [Text] / N. Bjorner [et al.] // Fields of Logic and Computation II. — Springer, 2015. — P. 24—51.
62. Fedyukovich, G. Competition Report: CHC-COMP-21 [Text] / G. Fedyukovich, P. Rummer // arXiv preprint arXiv:2109.04635. — 2021.
63. Frama-C [Text] / P. Cuoq [et al.] // International conference on software engineering and formal methods. — Springer. 2012. — P. 233—247.
64. Frama-C: A software analysis perspective [Text] / F. Kirchner [et al.] // For-mal Aspects of Computing. — 2015. — Vol. 27, no. 3. — P. 573—609.
65. The SeaHorn verification framework [Text] / A. Gurfinkel [et al.] // Inter-national Conference on Computer Aided Verification. — Springer. 2015. — P. 343-361.
66. Moving fast with software verification [Text] / C. Calcagno [et al.] // NASA Formal Methods Symposium. — Springer. 2015. — P. 3—11.
67. Kettl, M. The static analyzer Infer in SV-COMP (competition contribution) [Текст] / M. Kettl, T. Lemberger // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2022. — С. 451—456.
68. Build your own Resource Leak analysis [Текст]. — URL: https://github.com/facebook/infer/blob/main/infer/src/labs/README.md(дата обр. 30.05.2022).
69. Why don’t software developers use static analysis tools to find bugs? [Text] / B. Johnson [et al.] // 2013 35th International Conference on Software En-gineering (ICSE). - IEEE. 2013. - P. 672-681.
70. Anderson, P. Modernizing Static Analysis Tools to Facilitate Integrations [Text] / P. Anderson // ACM SIGAda Ada Letters. — 2020. — Vol. 39, no. 1. — P. 101—108.
71. Fanning, M. Static Analysis Results Interchange Format (SARIF) Version 2.0 [Текст] /M. Fanning, L. J. Golding. — 2019. — URL: https://docs.oasis-open.org/sarif/sarif/v2.0/sarif-v2.0.html(дата обр. 30.05.2022).
72. Anderson, P. Modernizing Static Analysis Tools to Facilitate Integrations [Text] / P. Anderson // Ada Lett. - New York, NY, USA, 2020. - Vol. 39, no. 1. - P. 101-108.
73. Compilers: Principles, Techniques, and Tools [Текст] / A. Aho [и др.]. — Pearson Addison-Wesley, 2014.
74. Cooper, K. Engineering a Compiler [Text] / K. Cooper, L. Torczon. — El-sevier Science, 2011.
75. Yelland, P. A New Approach to Optimal Code Formatting [Текст] / P. Yelland. — 2016. — Technical note for open source project rfmt; https://github.com/google/rfmt.
76. Hatton, L. Safer language subsets: an overview and a case history, MISRA C [Текст] / L. Hatton // Information and Software Technology. — 2004. — Т. 46, № 7. — С. 465—472.
77. Designing the McCAT compiler based on a family of structured intermediate representations [Текст] / L. Hendren [и др.] // International Workshop on Languages and Compilers for Parallel Computing. — Springer. 1992. — С. 406—420.
78. Merrill, J. GENERIC and GIMPLE: A new tree representation for entire functions [Text] / J. Merrill // Proceedings of the 2003 GCC Developers’ Summit. — Citeseer. 2003. — P. 171—179.
79. GNU Compiler Collection (GCC) internals: RTL [Текст]. — URL: https://gcc.gnu.org/onlinedocs/gccint/RTL.html(дата обр. 30.05.2022).
80. SUIF: An infrastructure for research on parallelizing and optimizing compilers [Текст] / R. P. Wilson [и др.] // ACM Sigplan Notices. — 1994. — Т. 29, № 12. — С. 31—37.
81. Soot - a Java Bytecode Optimization Framework [Текст] / R. Vallee-Rai [и др.] // Proceedings of the 1999 Conference of the Centre for Advanced Studies on Collaborative Research. — Mississauga, Ontario, Canada : IBM Press, 1999. — С. 13. — (CASCON ’99).
82. Arzt, S. Towards Cross-Platform Cross-Language Analysis with Soot [Text] / S. Arzt, T. Kussmaul, E. Bodden // Proceedings of the 5th ACM SIGPLAN International Workshop on State Of the Art in Program Analy¬sis. — Santa Barbara, CA, USA : Association for Computing Machinery,
2016. - P. 1-6. - (SOAP 2016).
83. Apache Commons BCEL [Текст]. — URL: https://commons.apache.org/proper/commons-bcel(дата обр. 10.06.2020).
84. Hovemeyer, D. Finding bugs is easy [Text] / D. Hovemeyer, W. Pugh // Acm sigplan notices. — 2004. — Vol. 39, no. 12. — P. 92—106.
85. An overview of AspectJ [Text] / G. Kiczales [et al.] // European Conference on Object-Oriented Programming. — Springer. 2001. — P. 327—354.
86. LLVM Language Reference [Текст]. — URL: https://llvm.org/docs/LangRef.html(дата обр. 01.02.2020).
87. Lattner, C. MLIR Primer: A Compiler Infrastructure for the End of Moore’s Law [Text] / C. Lattner, J. Pienaar. — 2019.
88. Abadi, M. A computational model for TensorFlow: an introduction [Text] / M. Abadi, M. Isard, D. G. Murray // Proceedings of the 1st ACM SIG¬PLAN International Workshop on Machine Learning and Programming Languages. — 2017. — P. 1—7.
89. CIL: Intermediate language and tools for analysis and transformation of C programs [Text] / G. C. Necula [et al.] // International Conference on Compiler Construction. — Springer. 2002. — P. 213—228.
90. Dillig, I. SAIL: Static analysis intermediate language with a two-level rep-resentation [Text] /1. Dillig, T. Dillig, A. Aiken // Technical report. — 2009.
91. Leino, K. R. M. This is Boogie 2 [Text] / K. R. M. Leino // manuscript KRML. — 2008. — Vol. 178, no. 131.
92. Torlak, E. Growing solver-aided languages with Rosette [Text] / E. Tor- lak, R. Bodik // Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software. — 2013. — P. 135—152.
93. Bonetta, D. GraalVM: metaprogramming inside a polyglot system (invited talk) [Text] / D. Bonetta // Proceedings of the 3rd ACM SIGPLAN Inter-national Workshop on Meta-Programming Techniques and Reflection. — 2018. — P. 3—4.
94. Bringing low-level languages to the JVM: efficient execution of LLVM IR on Truffle [Text] / M. Rigger [et al.] // Proceedings of the 8th International Workshop on Virtual Machines and Intermediate Languages. — 2016. — P. 6—15.
95. Wimmer, C. Truffle: a self-optimizing runtime system [Text] / C. Wimmer, T. Wurthinger // Proceedings of the 3rd annual conference on Systems, pro-gramming, and applications: software for humanity. — 2012. — P. 13—14.
96. Dullien, T. REIL: A platform-independent intermediate representation of disassembled code for static code analysis [Text] / T. Dullien, S. Porst. — 2009.
97. Yellin, F. The Java virtual machine specification [Text] / F. Yellin, T. Lind-holm. —1996.
98. Standard ECMA-335 - Common Language Infrastructure (CLI) [Текст]. — URL: http://www.ecma-international.org/publications/standards/Ecma-335.htm(дата обр. 30.05.2022).
99. Eagle, C. The IDA Pro Book, 2nd Edition [Text] / C. Eagle. — No Starch Press, 2011.
100. Eagle, C. The Ghidra Book: The Definitive Guide [Text] / C. Eagle,
K. Nance. — No Starch Press, 2020.
101. Mushtaq, Z. Multilingual source code analysis: A systematic literature re¬view [Text] / Z. Mushtaq, G. Rasool, B. Shehzad // IEEE Access. — 2017. — Vol. 5. - P. 11307-11336.
102. Pfeiffer, R.-H. Taming the Confusion of Languages [Text] / R.-H. Pfeif¬fer, A. Wqsowski // Modelling Foundations and Applications / ed. by
R. B. France [et al.]. — Berlin, Heidelberg : Springer Berlin Heidelberg, 2011. — P. 312—328.
103. Pfeiffer, R.-H. Language-Independent Traceability with Lassig [Text] /
R. -H. Pfeiffer, J. Reimann, A. Wqsowski // Modelling Foundations and Applications / ed. by J. Cabot, J. Rubin. — Cham : Springer International Publishing, 2014. - P. 148-163.
104. Pangea: A Workbench for Statically Analyzing Multi-language Software Corpora [Text] / A. Caracciolo [et al.] // 2014 IEEE 14th International Work-ing Conference on Source Code Analysis and Manipulation. — 2014. — P. 71—76.
105. Storm, T. van der. The Rascal language workbench [Text] / T. van der Storm // CWI. Software Engineering [SEN]. — 2011. — Vol. 13. — P. 14.
106. Зубов, М. В. Применение универсальных промежуточных представлений для статического анализа исходного программного кода [Текст] / М. В. Зубов, А. Н. Пустыгин, Е. В. Старцев // Доклады Томского государственного университета систем управления и радиоэлектроники. — 2013. - 1 (27). - С. 64-68.
107. Emerson, E. A. Characterizing correctness properties of parallel programs using fixpoints [Text] / E. A. Emerson, E. M. Clarke // International Collo-quium on Automata, Languages, and Programming. — Springer. 1980. — P. 169—181.
108. Browne, M. C. Characterizing finite Kripke structures in propositional tem-poral logic [Text] / M. C. Browne, E. M. Clarke, O. Grumberg // Theoretical computer science. — 1988. — Vol. 59, no. 1/2. — P. 115—131.
109. Kripke, S. A. Semantical Considerations on Modal Logic [Text] /
S. A. Kripke // Acta Philosophica Fennica. — 1963. — Vol. 16.
110. Holzmann, G. The Spin Model Checker: Primer and Reference Manual [Text] / G. Holzmann. — Addison-Wesley, 2004.
111. ACSL: ANSI/C specification language [Text] / P. Baudin [et al.] // CEA- LIST, Saclay, France, Tech. Rep. v1. — 2008. — Vol. 2.
112. Filliatre, J.-C. The Why/Krakatoa/Caduceus platform for deductive pro¬gram verification [Text] / J.-C. Filliatre, C. Marche // International Confer¬ence on Computer Aided Verification. — Springer. 2007. — P. 173—177.
113. Beningo, J. Documenting Firmware with Doxygen [Text] / J. Beningo // Reusable Firmware Development. — Springer, 2017. — P. 121—148.
114. Itsykson, V. Automated program transformation for migration to new libraries [Text] / V. Itsykson, A. Zozulya // 2011 7th Central and Eastern Eu-ropean Software Engineering Conference (CEE-SECR). — IEEE. 2011. — P. 1—7.
115. Meyer, B. Design by contract [Text] / B. Meyer. — Prentice Hall Upper Saddle River, 2002.
116. The Java Modelling Language (JML) [Текст]. — URL: http://www.eecs.ucf.edu/~leavens/JML/index.shtml(дата обр. 30.05.2022).
117. Pnueli, A. The temporal logic of programs [Text] / A. Pnueli // 18th Annual Symposium on Foundations of Computer Science (SFCS 1977). —1977. — P. 46-57.
118. Pnueli, A. The temporal semantics of concurrent programs [Text] / A. Pnueli // Theoretical computer science. — 1981. — Vol. 13, no. 1. — P. 45—60.
119. Buchi, J. R. On a decision method in restricted second order arithmetic [Text] / J. R. Buchi // The Collected Works of J. Richard Buchi. — Springer, 1990. — P. 425—435.
120. Emerson, E. The design and synthesis of synchronization skeletons using temporal logic [Text] / E. Emerson // Workshop on Logics of Programs. Vol. 131. - 1981. - P. 52-72.
121. Symbolic model checking without BDDs [Text] / A. Biere [et al.] // Interna-tional conference on tools and algorithms for the construction and analysis of systems. — Springer. 1999. — P. 193—207.
122. De Moura, L. Satisfiability modulo theories: introduction and applications [Text]/L. De Moura, N. Bjorner//Communications of the ACM. —2011.— Vol. 54, no. 9. — P. 69—77.
123. DPLL (T): Fast decision procedures [Text] / H. Ganzinger [et al.] // Inter-national Conference on Computer Aided Verification. — Springer. 2004. — P. 175—188.
124. Marques Silva, J. P. GRASP—a new search algorithm for satisfiability [Text] / J. P. Marques Silva, K. A. Sakallah // The Best of ICCAD. — Springer, 2003. - P. 73-89.
125. Rival, X. Introduction to Static Analysis: An Abstract Interpretation Per-spective [Text] / X. Rival, K. Yi. — MIT Press, 2020.
126. Komuravelli, A. SMT-based model checking for recursive programs [Text] / A. Komuravelli, A. Gurfinkel, S. Chaki // Formal Methods in System De-sign. - 2016. - Vol. 48, no. 3. - P. 175-205.
127. Kostyukov, Y. Beyond the elementary representations of program invari¬ants over algebraic data types [Text] / Y. Kostyukov, D. Mordvinov, G. Fedyukovich // Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. — 2021. — P. 451—465.
128. RInGen: Regular Invariant Generator [Текст]. — URL: https://github.com/Columpio/RInGen(дата обр. 30.05.2022).
129. A survey of symbolic execution techniques [Text] / R. Baldoni [et al.] // ACM Computing Surveys (CSUR). — 2018. — Vol. 51, no. 3. — P. 1—39.
130. Klee: unassisted and automatic generation of high-coverage tests for com-plex systems programs. [Text] / C. Cadar, D. Dunbar, D. R. Engler, [et al.] // OSDI. Vol. 8. - 2008. - P. 209-224.
131. UnitTestBot [Текст]. — URL: https://unittestbot.github.io (дата обр. 30.05.2022).