Автоматическое обнаружение дефектов в многопоточных программах методами статического анализа тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат технических наук Моисеев, Михаил Юрьевич

• Моисеев, Михаил Юрьевич
• кандидат технических наук
• 2011

Оглавление диссертации кандидат технических наук Моисеев, Михаил Юрьевич

ВВЕДЕНИЕ.

ГЛАВА 1. СРАВНИТЕЛЬНЫЙ АНАЛИЗ СУЩЕСТВУЮЩИХ МЕТОДОВ И СРЕДСТВ ОБНАРУЖЕНИЯ ОШИБОК В МНОГОПОТОЧНЫХ ПРОГРАММАХ.

1.1. Критерии оценки методов и средств обнаружения ошибок.

1.2. Общие подходы к анализу параллельных программ.

1.2.1. Подходы на основе анализа частичных порядков.

1.2.2. Подходы на основе анализа наборов конструкций синхронизации.

1.2.3. Подходы на основе извлечения инвариантов.

1.2.4. Подходы на основе преобразования к последовательной программе.

1.3. Методы обнаружения ошибок в многопоточных программах.

1.3.1. Комбинирование алгоритмов анализа.

1.3.2. Использование аппроксимаций.

1.4. Средства обнаружения ошибок в многопоточных программах на языке С.

Выводы.

ГЛАВА 2. МОДЕЛЬ МНОГОПОТОЧНОЙ ПРОГРАММЫ И ПРЕДСТАВЛЕНИЕ РЕЗУЛЬТАТОВ СТАТИЧЕСКОГО АНАЛИЗА.

2.1. Общая структура предлагаемого подхода.

2.2. Модель многопоточной программы.

2.2.1 Объекты и функции РЙггеаёз.

2.2.2 Представление объектов и функций РЙ1геасЬ в модели программы.

2.3. Представление динамических свойств многопоточной программы

2.3.1. Состояние программы.

2.3.2. Представление информации о параллельном выполнении программы.

ГЛАВА 3. МЕТОДЫ АНАЛИЗА ПАРАЛЛЕЛЬНОГО ВЫПОЛНЕНИЯ

ПРОГРАММЫ.

3.1. Организация совместного выполнения алгоритмов анализа.

3.2. Алгоритм определения действий над объектами синхронизации.

3.3. Алгоритм определения состояний объектов синхронизации.

3.3.1 Способы построения допустимых комбинаций.

3.3.2 Построение неполных комбинаций.

3.3.3 Правила расчета состояний объектов синхронизации.

3.3.4 Анализ конструкции state.

3.4. Алгоритм построения отношений параллельности.

3.5. Алгоритм построения отношений синхронизации.

3.6. Алгоритм учета взаимного влияния потоков программы.

3.7. Итеративный алгоритм анализа конструкций.

3.7.1 Правила работы итеративного алгоритма.

3.7.2 Завершимость итеративного алгоритма.

3.7.3 Сохранение полноты результатов анализа.

ГЛАВА 4. АЛГОРИТМЫ ОБНАРУЖЕНИЯ ОШИБОК В МНОГОПОТОЧНЫХ ПРОГРАММАХ.

4.1 Классификация программных ошибок.

4.2 Правила обнаружения программных дефектов.

4.2.1 Правила обнаружения ошибок управления ресурсами и динамической памятью.

4.2.2 Правила обнаружения утечек ресурсов и памяти.

4.2.3 Правила обнаружения ошибок работы с буферами.

4.2.4 Правила обнаружения ошибок отсутствия инициализации

4.2.5 Правила обнаружения ошибок синхронизации.

4.3 Обнаружение множественных дефектов.

ГЛАВА 5. ПРАКТИЧЕСКАЯ РЕАЛИЗАЦИЯ И ОЦЕНКА ЭФФЕКТИВНОСТИ РАЗРАБОТАННЫХ МЕТОДОВ.

5.1 Реализация разработанных методов.

5.2 Проведение экспериментальных исследований.

5.3 Оценки полноты и точности.

5.4 Оценка вычислительной сложности.

5.4.1 Вычислительная сложность правил, использующих допустимые комбинации.

5.4.2 Вычислительная сложность итеративного алгоритма.

5.4.3 Сравнение с существующими подходами.

Введение диссертации (часть автореферата) на тему «Автоматическое обнаружение дефектов в многопоточных программах методами статического анализа»

Актуальность работы

В настоящее время как никогда остро стоит проблема повышения качества программного обеспечения [10]. Это связано с тем, что все большее число технических систем используют программные компоненты. Программные системы могут решать сложные и ответственные задачи, при этом практически все они содержат ошибки. Одним из видов ошибок в ПО являются нефункциональные ошибки - ошибки, связанные с нарушениями правил языка программирования, некорректным использованием библиотечных функций и системных вызовов и т.п.

Большая часть системного ПО, а также ПО для мобильных и встраиваемых систем, систем управления и других критически важных приложений создается с использованием языка С. По данным компании Соуег^у в программах на языке С, в среднем, содержится 0.25 нефункциональных ошибок на 1000 строк исходного кода [5]. Нефункциональные ошибки, характерные для последовательных программ, принято называть программными дефектами. Наиболее распространенными типами программных дефектов в программах на языке С являются [3]:

• разыменование некорректного или нулевого указателя,

• переполнение буфера и выход за границы объекта,

• использование неинициализированной переменной,

• утечки и повторное освобождение ресурсов.

Проявление программных дефектов может приводить к выдаче неверных результатов, зависанию или аварийному завершению программы, нарушению конфиденциальности хранимой информации.

Обнаружение и исправление программных дефектов (отладка программы) является одной из самых сложных и трудоемких задач в процессе разработки ПО. При этом, по некоторым оценкам, на обнаружение дефекта тратится до 95% времени отладки, на его исправление - только 5%. Все это делает задачу автоматизации процесса обнаружения программных дефектов актуальной.

Исследования в области автоматизации обнаружения программных дефектов ведутся начиная с момента появления первых программ. Для оценки эффективности методов обнаружения дефектов используются следующие количественные показатели [31]:

• полнота - доля обнаруженных дефектов среди всех дефектов имеющихся в программе,

• точность - д оля истинных дефектов среди всех обнаруженных дефектов,

• степень автоматизации - трудоемкость и сложность применения метода,

• ресурсоемкость - количество выполняемых операций и необходимый объем памяти.

Современные методы автоматизированного обнаружения программных дефектов, можно разделить на следующие классы [15, 62]:

• динамические методы — используют результаты выполнения программы,

• статические методы - используют исходный код программы, модели программы, спецификации и другие артефакты, создаваемые в процессе проектирования,

• синтетические (гибридные) методы — сочетают несколько разных методов.

К динамическим методам относятся: мониторинг, различные виды тестирования, анализ трасс выполнения и др. Использование динамических методов обеспечивает получение точных результатов. Основными недостатками динамических методов являются: неполнота получаемых результатов и невозможность полной автоматизации процесса обнаружения.

К статическим методам относятся методы проверки моделей, методы дедуктивной верификация и методы статического анализа. Методы проверки моделей [60, 61] гарантируют обнаружение нарушений спецификации, обеспечивают получение полных и точных результатов, позволяют анализировать параллельные программы и обнаруживать ошибки синхронизации. Основными недостатками этих методов являются необходимость ручного построения модели программы и высокая ресурсоемкость алгоритмов. Методы дедуктивной верификация [43] позволяют строго доказывать определенные свойства программы и могут применяться для обнаружения программных дефектов. Однако, существующие методы дедуктивной верификации допускают лишь частичную автоматизацию и требуют высокой квалификации пользователя. Обнаружение программных дефектов на основе методов статического анализа [41, 21] представляется наиболее перспективным подходом. Применение статического анализа позволяет обнаруживать все основные типы программных дефектов, при этом обеспечивается получение полных результатов. Еще одним преимуществом статического анализа является возможность полной автоматизации процесса обнаружения дефектов.

Методы статического анализа широко применяется для оптимизации последовательных и параллельных программ, маскирующих преобразований и выявления уязвимостей защиты программ, автоматизации обнаружения программных ошибок [56]. В настоящее время существуют эффективные методы статического анализа, обеспечивающие обнаружение дефектов в последовательных программах, однако многие программные системы используют те или иные механизмы распараллеливания. Одним из широко распространенных классов параллельных программ являются многопоточные программы. В многопоточных программах кроме программных дефектов, могут встречаться ошибки синхронизации -нефункциональные ошибки, связанные с неправильной организацией параллельного выполнения программы. Основными типами ошибок синхронизации являются:

• конкурентная модификация и использование данных (разделяемых объектов) из разных потоков программы (Race Condition),

• блокировки и взаимные блокировки потоков (Deadlock),

• некорректное использование функций синхронизации (Blocking Call Misuse).

Применение алгоритмов статического анализа, не учитывающих специфику многопоточных программ, приводит к снижению полноты и точности получаемых результатов, а также не позволяет обнаруживать ошибки синхронизации.

Исследования, посвященные обнаружению программных дефектов в параллельных (многопоточных) программах на основе статического анализа, ведутся в ряде отечественных (ИСП РАН, СПбГУ, СПбГПУ, СПбГУИТМО, МФТИ, МГУ и др.) и зарубежных университетов (MIT, Stanford University, University of California, University of Cambridge, Cornell University и др.), a также в научно-исследовательских центрах (Microsoft Research, Intel Research, HP Laboratories, NEC Laboratories и др.). Существующие методы статического анализа многопоточных программ на языке С решают только часть задач, необходимых для обнаружения программных дефектов и обладают рядом недостатков: анализируется ограниченное подмножество конструкций языка, имеются ограничения на способы синхронизации потоков, используются аппроксимации программы, приводящие к недостаточной полноте и точности получаемых результатов.

Большое количество проводимых исследований, а также недостаточная степень проработки и ограничения существующих методов, свидетельствуют о том, что задача разработки и реализации методов обнаружения дефектов в многопоточных программах на основе статического анализа является актуальной. В данной работе рассматриваются многопоточные программы на языке С. Актуальность разработки методов обнаружения дефектов для программ на языке С обусловлена высокой популярностью этого языка [17], а также большим количеством программ и библиотек, написанных на этом языке.

Цель работы

Целью данной работы является исследование и разработка методов автоматизации обнаружения программных дефектов в многопоточных программах на основе статического анализа.

Задачи исследования

Основными задачами исследования являются:

1. Анализ существующих подходов к обнаружению дефектов в многопоточных программах на основе статического анализа.

2. Разработка модели многопоточной программы.

3. Выбор алгоритмов статического анализа, обеспечивающих извлечение необходимой информации для обнаружения программных дефектов.

4. Разработка алгоритмов анализа параллельного выполнения многопоточной программы.

5. Организация взаимодействия отдельных алгоритмов анализа.

6. Выбор и уточнение алгоритмов обнаружения программных дефектов на основе результатов статического анализа.

7. Реализация прототипа системы автоматического обнаружения дефектов в многопоточных программах на языке С.

Методы исследования

При проведении теоретических исследований применяются методы теории множеств, теории графов, теории отношений, теории решеток, абстрактной интерпретации, статического анализа. При разработке прототипа системы автоматического обнаружения дефектов используются методы объектно-ориентированного анализа и проектирования.

Научная новизна работы

Научная новизна работы заключается в следующем:

1. Разработан метод получения информации о параллельном выполнении многопоточной программы, определяющий параллельно выполняющиеся блоки программы, взаимодействующие конструкции синхронизации, а также состояния объектов синхронизации. Построение допустимых комбинаций блоков программы при анализе конструкций синхронизации обеспечивает повышение точности результатов.

2. Разработан метод совместного анализа потоков программы, обеспечивающий корректный анализ многопоточных программ, использующих разделяемые объекты, а также программ с несколькими возможными порядками выполнения конструкций. Данный метод управляет последовательностью анализа конструкций и распространяет изменения значений разделяемых объектов между потоками программы. Определение актуальных значений разделяемых объектов обеспечивает повышение точности результатов.

3. Предложен способ организации совместного выполнения алгоритмов анализа многопоточной программы, позволяющий расширить алгоритмы анализа последовательных программ на класс многопоточных программ. Данный способ обеспечивает учет всех взаимодействий между используемыми алгоритмами, что позволяет сохранить полноту получаемых результатов. Обмен промежуточными данными между всеми алгоритмами в процессе анализа обеспечивает повышение точности получаемых результатов.

На защиту выносится метод получения информации о параллельном выполнении многопоточной программы, метод совместного анализа потоков программы, а также предложенный способ организации совместного выполнения алгоритмов анализа многопоточной программы.

Достоверность результатов

Достоверность теоретических результатов подтверждается доказательствами утверждений, лежащих в основе разработанных методов, а также экспериментальными результатами, полученными при исследовании разработанного прототипа системы обнаружения программных дефектов.

Практическая значимость работы

Разработанные методы предназначены для автоматизации обнаружения программных дефектов в многопоточных программах на языке С. Применение этих методов позволит повысить качество как вновь разрабатываемых, так и уже существующих программных систем, а также снизить трудоемкость и сократить сроки отладки ПО.

Реализованный в рамках данной работы прототип средства обнаружения дефектов позволяет обнаруживать основные типы программных дефектов и некоторые типы ошибок синхронизации в многопоточных программах на языке С, использующих потоки и объекты синхронизации Р^еаёБ.

Теоретические и практические результаты диссертационной работы могут являться основой для разработки промышленного средства обнаружения программных дефектов.

Реализация результатов работы

Реализацией результатов работы является прототип средства обнаружения дефектов, который может применяться для повышения качества многопоточных программ на языке С.

Результаты работы используются в системе обнаружения ошибок синхронизации в программах на языке 8уз1етС, разработанной в рамках НИР по заказу ЗАО «Интел А/О» в 2010 году, имеется акт о внедрении.

Апробация работы

Основные идеи и результаты работы докладывались на конференциях «Software Engineering Conference in Russia 2010», «Approaches and tools for efficient design of reconfigurable/programmable SOC. Intel Workshop in Saint-Petersburg 2010», «Технологии Microsoft в теории и практике программирования», «Software Engineering Conference in Russia 2009», a также обсуждались на семинарах кафедры КСПТ, СПбГПУ и кафедры системного программирования, СПбГУ.

Публикации

По результатам диссертационной работы опубликовано 9 печатных работ, в том числе в журналах «Научно-технические ведомости СПбГПУ» и «Информационно-управляющие системы» (входят в «Перечень ведущих рецензируемых научных журналов и изданий, выпускаемых в Российской Федерации»). Основные результаты диссертационной работы изложены в статье «Автоматическое обнаружение дефектов в многопоточных программах методами статического анализа» опубликованной в журнале «Научно-технические ведомости СПбГПУ» в 2010 году. Всего по теме работы опубликовано 5 журнальных статей и 4 тезиса конференций.

Структура и объем работы

Диссертационная работа состоит из введения, пяти глав, заключения, списка используемых источников. Общий объем работы составляет 173 печатные страницы, работа включает 73 рисунка, список источников из 65 наименований, 4 приложения.

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Моисеев, Михаил Юрьевич

Основные результаты работы заключаются в следующем:

1. Разработана модель многопоточной программы на языке С, представляющая исходный код программы в удобном для проведения статического анализа виде. Для представления функций над потоками и объектами синхронизации в модели программы используется разработанный базис конструкций управления параллельным выполнением.

2. Для представления динамических свойств многопоточной программы, извлекаемых при проведении статического анализа, разработан формализм, включающий состояние обычных объектов программы и информацию о параллельном выполнении программы. Информация о параллельном выполнении программы включает состояния объектов синхронизации, отношения параллельности и отношения синхронизации между блоками программы.

3. Разработан метод получения информации о параллельном выполнении многопоточной программы, выполняющий построение отношений параллельности и синхронизации, а также определение состояний объектов синхронизации. Данный метод является основой для расширения алгоритмов статического анализа последовательных программ на многопоточные программы, обеспечивая сохранение полноты получаемых результатов. Использование допустимых комбинаций блоков программы обеспечивает повышение точности результатов анализа.

4. Разработан метод совместного анализа потоков программы, выполняющий распространение изменений состояния программы между потоками и управление последовательностью анализа конструкций программы. Данный метод обеспечивает сохранение полноты результатов при анализе многопоточных программ, использующих разделяемые объекты, а также для программ с несколькими возможными порядками выполнения конструкций. Определение актуальных значений разделяемых объектов обеспечивает повышение точности получаемых результатов.

5. Предложен способ организации совместного выполнения алгоритмов статического анализа многопоточной программы. Данный способ обеспечивает учет всех взаимодействий между алгоритмами, что позволяет сохранить полноту получаемых результатов. Обмен промежуточными данными между алгоритмами в процессе анализа обеспечивает повышение точности получаемых результатов.

6. Разработанные методы реализованы в прототипе средства автоматического обнаружения программных дефектов в многопоточных программах на языке С.

Разработанные методы и система обнаружения дефектов Aegis МТ удовлетворяют всем требованиям, сформулированным в разделе 1.1. Разработанные методы позволяют выполнять анализ обычных объектов программы и объектов синхронизации, обеспечивая извлечение необходимой информации для обнаружения широкого класса программных дефектов и некоторых видов ошибок синхронизации. Разработанные методы не имеют ограничений на число анализируемых потоков и объектов синхронизации, при этом обеспечивается идентификация объектов в разных потоках программы. Предложенный способ организации совместного выполнения алгоритмов анализа обеспечивает обмен результатами между всеми алгоритмами.

Разработанная система обнаружения дефектов Aegis МТ обеспечивает полную поддержку языка С стандарт С99 [6] и позволяет выполнять анализ многопоточных программ на основе Pthreads. Получение полных результатов, при анализе многопоточных программ, обеспечивается в случае использования основных алгоритмов статического анализа, обладающих полнотой. Возможность получения полных результатов подтверждается экспериментальными исследованиями разработанной системы Aegis МТ. Оценка точности результатов, полученная экспериментально, является достаточно высокой (20%), что позволяет говорить о возможности применения разработанного средства для повышения качества промышленного ПО. v

Разработанные методы и алгоритмы могут применяться при проектировании средств анализа многопоточных программ с целью обнаружения различного вида нефункциональных и функциональных ошибок, а также для оценки различных характеристик выполнения программы, оптимизации, реверс-инжениринга. Разработанные методы могут быть расширены на другие библиотеки организации многопоточности и другие языки программирования. На основе этих методов создано средство автоматического обнаружения ошибок синхронизации для аппаратных моделей на языке SystemC.

Основными ограничениями разработанного подхода являются ограничения на класс анализируемых многопоточных программ:

1. анализируются программы с явной синхронизацией потоков — для синхронизации используются только функции над объектами синхронизации (не используется синхронизация на основе обычных переменных атомарных типов, специальных объектов ОС и т.п.).

2. анализируются программы, в которых отсутствуют ошибки синхронизации следующих типов: ошибки использования функций синхронизации, и ошибки блокировки потоков программы (см. раздел 4).

Первое ограничение не является существенным, так как общепринятые правила создания многопоточных программ предписывают использовать способы синхронизации, основанные только на вызове функций над объектами синхронизации. Второе ограничение предлагается преодолевать за счет обнаружения ошибок синхронизации указанных типов и выдачи соответствующих предупреждений. Подразумевается, что выданные предупреждения будут проверены пользователем, при наличии ошибок, эти ошибки будут исправлены и анализ программы будет выполнен повторно. Выполнение анализа программы с помощью разработанных методов при наличии ошибок синхронизации, может приводить к снижению полноты и точности результатов.

Ограничениями средства обнаружения дефектов Aegis МТ являются поддержка только двух типов объектов синхронизации — мьютекса и семафора, а также отсутствие поддержки других способов создания многопоточных программ кроме Pthreads и других языков программирования кроме языка С.

Можно определить следующие направления развития разработанных методов и системы обнаружения дефектов Aegis МТ:

1. Проведение дополнительных экспериментальных исследований с целью уточнения показателей эффективности разработанных методов и сравнения с другими средствами автоматизации обнаружения дефектов.

2. Уточнение и доработка алгоритмов анализа, в частности, реализация анализа зависимостей между состоянием объекта синхронизации и значениями объектов программы.

3. Поддержка всех основных типов объектов синхронизации Pthreads, в том числе, объектов RWLock и переменных состояния.

4. Расширение перечня обнаруживаемых ошибок синхронизации, в частности, обнаружение ошибок взаимной блокировки потоков.

5. Расширение разработанных методов и средства на другие способы создания многопоточных программ и другие языки программирования.

ЗАКЛЮЧЕНИЕ

Список литературы диссертационного исследования кандидат технических наук Моисеев, Михаил Юрьевич, 2011 год

1. AEGIS Defect Detection System Electronic Resource. / Digitek Labs. — http://www.digitek-labs.ru/aegis/

2. Boost С++ libraries Electronic Resource. / Официальный сайт . — http://www.boost.org/.

3. CERT С Secure Coding Standard Electronic Resource. / Carnegie Mellon University : 2008. https://www.securecoding.cert.org/confluence/display/seccode/CERT+C+Se cure+Coding+Standard

4. Coverity Static Analysis Electronic Resource. / Компания Coverity. — http://www.coverity.com/products/static-analysis.html

5. OPEN SOURCE REPORTS 2008 and 2009 Electronic Resource. / Компания Coverity. — http://www.scan.coverity.com/report/.

6. С Language Standard ISO/IEC 9899:1990 Electronic Resource. / Официальный сайт международной организации стандартизации. — http://www.iso. org/iso/cataloguedetail.htm?csnumber= 17782.

7. GCC, the GNU Compiler Collection Electronic Resource. / GNU Project. — http:// gcc. gnu.org/.

8. IBM Software Analyzer Electronic Resource. / Официальный сайт компании IBM. — http://www-01 .ibm.com/software/awdtools/swanalyzer/

9. IEEE 1003. IEEE Standards Electronic Resource. / Официальный сайт ассоциации стандартов IEEE. — http://standards.ieee.org/.

10. ISO/IEC 9126. ISO Standards Electronic Resource. / Официальный сайт международной организации стандартизации. — http://www.iso.org/iso/isocatalogue/cataloguetc/cataloguedetail.htm7csn umber=50516.

11. ISO/IEC 9945. ISO Standards Electronic Resource. / Официальный сайт международной организации стандартизации. —http://www.iso.org/iso/iso catalogue/cataloguetc/catalogue detail.htm?csn umber=50516.

12. Klocwork Insight Electronic Resource. / Официальный сайт компании Klocwork. — http://www.klocwork.com

13. The OpenMP API specification for parallel programming Electronic Resource. / Официальный сайт OpenMP. — http://openmp.org/wp/openmp-specifications/.

14. Parasoft С++ test Electronic Resource. / Официальный сайт компании Parasoft. — http://www.parasoft.com

15. SWEBOK Guide to the Software Engineering Body of Knowledge — 2004 Version. — Washington: IEEE Computer Society, 2004.

16. Intel Th reading В uilding В locks Electronic R esource. / Официальный сайт. —■ http://threadingbuildingblocks.org/.

17. TIOBE Software: The Coding Standards Company / Официальный сайт компании TIOBE. — http://www.tiobe.com/index.php/content/company/Home.html

18. Bouajjani A., Esparza J., Touili T. A Generic Approach to the Static Analysis of Concurrent Programs with Procedures // Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. — New York: ACM, 2003. — p. 62-73.

19. From Single Thread to Multithreaded: An Efficient Static Analysis Algorithm Electronic Resource. / Carre J-L., Hymans C.: 2009. — http://arxiv.org/PS cache/arxiv/pdff0910/0910.5 833v 1 .pdf

20. Chess В., West J. Secure Programming with Static Analysis. — Addison-Wesley, 2007. —619 p.

21. Callahan D., Kennedy K., Subhlok J. Analysis of Event Synchronization in Parallel Programming Tool // Proceedings of the second ACM SIGPLAN symposium on Principles & practice of parallel programming. — New York: ACM, 1990. —p. 21-30.

22. Chugh R., Voung J., Jhala R., Lerner S. Dataflow Analysis for Concurrent Programs using Datarace Detection // Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation. —New York: ACM, 2008. — p. 316-326.

23. Cytron R., Ferrante J., Rosen B. et al. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph // In ACM Transactions on Programming Languages and Systems. — New York: ACM, 1991. —p. 451-490.

24. Emrath P., Ghosh S., Padua D. Event Synchronization Analysis for Debugging Parallel Programs // In Proceedings of Supercomputing '89. — New York: ACM, 1989. — p. 580-588.

25. Emrath P., Ghosh S., Padua D. Detecting Nondeterminacy in Parallel-Programs // In IEEE Software, v.9, n.l. — Washington: IEEE Computer Society, 1992—p. 69-77.

26. Emmi M., Qadeer S., Rakamaric Z. Delay-Bounded Scheduling // Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. — New York: ACM, 2011. — p. 174-186.

27. Engler D., Ashcraft K. RacerX: Effective, Static Detection of Race Conditions and Deadlocks // Proceedings of the nineteenth ACM symposium on Operating systems principles. — New York: ACM, 2003. — p. 237-252.

28. Godefroid P. Model checking for programming languages using VeriSoft // Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. — New York: ACM, 1997. — p. 174-186.

29. Gotsman A., Berdine J., Cook B., Sagiv M. Thread-Modular Shape Analysis // Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation. — New York: ACM, 2007. —p. 266-277.

30. Jackson D., Rinard M. Software Analysis: A Roadmap // Proceedings of the Conference on The Future of Software Engineering. — New York: ACM, 2000, —p. 133-145.

31. Ladkin P., Simons B. Static Analysis of Interprocess Communication. Lecture Notes in Computer Science. — Berlin: Springer, 1995. — 145 p.

32. Lai A., Reps T. Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis // Formal Methods in System Design. — New York: ACM, 2009. —p. 73-97.

33. Lahiri S., Qadeer S., Rakamaric Z. Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers // In Computer Aided Verification — Berlin: Springer, 2009. — p. 73-97.

34. Naik M., Park C., Sen K., Gay D. Effective Static Deadlock Detection // Proceedings of the 31st International Conference on Software Engineering. — Washington: IEEE Computer Society, 2009. — p. 386-396.

35. Naik M., Aiken A. Conditional Must Not Aliasing for Static Race Detection // Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. — New York: ACM, 2007. — p. 327-338.

36. Naik M. Effective Static Race Detection for Java. PhD thesis, Stanford University, 2008.

37. Nielson F., Nielson H.R., Hankin C. Principles of Program Analysis. — Berlin: Springer, 2005. — 452 p.

38. Netzer R., Ghosh S. Efficient race condition for shared-memory programs with post/wait synchronization // International Conference on Parallel Processing. — 1992. — p. 242-246.

39. Peled D. Software Reliability Methods — Berlin: Springer-Verlag, 2001. — 331 p.

40. Pratikakis P., Foster J., Hicks M. LOCKSMITH: Context-Sensitive Correlation Analysis for Race Detection // Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation. — New York: ACM, 2006. — p. 320-331.

41. Pratikakis P., Foster J., Hicks M. LOCKSMITH: Practical Static Race Detection for C // Journal ACM Transactions on Programming Languages and Systems, Volume 33, Issue 1. —New York: ACM, 2011.

42. Qadeer S., Wu D. KISS: Keep It Simple and Sequential // Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation. —New York: ACM, 2004. — p. 14-24.

43. Qadeer S., Rajamani S., Rehof J. Summarizing procedure in Concurrent Programs // Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages. — New York: ACM, 2004. — p. 245-255.

44. Ramanujam J., Mathew A. Analysis of Event Synchronization in Parallel Programs // In Languages and Compilers for Parallel Computing. — Berlin: Springer, 1995. — p. 300-315.

45. Rinard M. Analysis of Multithreaded Programs // Lecture Notes in Computer Science, Vol. 2126/2001. — Berlin: Springer, 2001. — p. 1-19.

46. Lecture Notes on Static Analysis Electronic Resource. / Schwartzbach M.: 2000. — lara.epfl.ch/web2010/media/sav08:schwartzbach.pdf.

47. Terauchi T. Checking Race Freedom via Linear Programming // Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation. —New York: ACM, 2008. —p. 1-10.

48. Torre S., Madhusudan P., Parlato G. Reducing Context-Bounded Concurrent Reachability to Sequential Reachability // Proceedings of the 21st International Conference on Computer Aided. — Berlin: Springer, 2009.—p. 477-492.

49. Исследование и разработка системы автоматического обнаружения дефектов в исходном коде программного обеспечения. Выбор направлений исследований: отчет о НИР / СПбГПУ, Рудекой А.И.— СПб., 2008.— С. 136. № ГР 0120.0 808661. -Инв. № 02 2009 00405.

50. Гайсарян С.С., Чернов А.В., Белеванцев А.А. и др. О некоторых задачах анализа и трансформации программ // Труды Института системного программирования РАН, 2004.

51. Ицыксон В.М., Моисеев М.Ю., Захаров A.B. и др. Алгоритм интервального анализа для обнаружения дефектов в исходном коде программ // Информационные и управляющие системы. № 2 (39). — СПб.: Политехника, 2009. —с. 34-41.

52. Ицыксон В.М., Глухих М.И. ' Язык спецификаций поведения программных компонентов // Научно-технические ведомости СПбГПУ

53. СПб.: СПбГПУ, 2010. №3. — с. 63-70.

54. Карпов Ю.Г. Model Checking. Верификация параллельных и распределенных программных систем. — СПб.: БХВ-Петербург, 2010.552 с.

55. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. — М.: МЦНМО, 2002. — 416 с.

56. Кулямин В.В. Методы верификации программного обеспечения // Всероссийский конкурсный отбор обзорно-аналитических статей по приоритетному направлению "Информационно-телекоммуникационные системы", 2008. — 117 с.

57. Моисеев М.Ю. Итеративный алгоритм статического анализа для обнаружения дефектов в исходном коде программ // Информационные и управляющие системы. — Политехника, 2009. №3. — с. 33-39.

58. Моисеев М.Ю., Ицыксон В.М., и др. Исследование средств автоматизации обнаружения дефектов в исходном коде программ // Научно-технические ведомости СПбГПУ — СПб.: СПбГПУ, 2008. №5.с. 119-127.

59. Несов B.C., Маликов О.Р. Использование информации о линейных зависимостях для обнаружения уязвимо стей в исходном коде программ // Труды Института системного программирования РАН, 2006.