Верификация С-программ с помощью смешанной аксиоматической семантики тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Марьясов, Илья Владимирович

• Марьясов, Илья Владимирович
• кандидат физико-математических наук
• 2012

Оглавление диссертации кандидат физико-математических наук Марьясов, Илья Владимирович

Оглавление

Введение

Глава

Языки программ и спецификаций

1.1 Язык С-Н

1.2 Язык С-кегпе1

1.3 Язык утверждений

1.3.1 Типы и алфавит

1.3.2 Выражения

1.3.3 Подстановка

1.3.4 Интерпретация выражений

1.3.5 Логические утверждения

Глава

Модифицированная операционная семантика языка С-Н^

2.1 Абстрактная машина языка С-Н^

2.2 Параметры и абстрактные функции

2.3 Аксиомы и правила вывода

2.4 Семантика частичной корректности

2.5 Трансляция языка в С-кегпе1

2.5.1 Перевод операторов и деклараций

2.5.2 Перевод выражений

Глава

Смешанная аксиоматическая семантика языка С-кегпе1

3.1 Предварительные понятия

3.2 Выражения

3.3 Декларации

3.4 Операторы

3.5 Другие правила

3.6 Перевод инвариантов из С-Н^ в С-кегпе1

Глава

Непротиворечивость смешанной аксиоматической семантики

4.1 Предварительные понятия

4.2 Теорема о непротиворечивости

Глава

Примеры применения смешанной аксиоматической семантики

5.1 Вычисление факториала

5.2 Поиск в линейном односвязном списке

5.3 Топологическая сортировка

Заключение

Литература

Введение диссертации (часть автореферата) на тему «Верификация С-программ с помощью смешанной аксиоматической семантики»

Введение

В диссертации представлены формальные семантики языков C-light и C-kernel, ориентированные на верификацию методом Хоара. Доказана теорема о корректности аксиоматической семантики языка C-kernel, исследован вопрос перехода инвариантов циклов при трансляции программ из языка С-light в язык C-kernel, приведены примеры, иллюстрирующие применение предложенных семантик. Актуальность темы

Формальная верификация программ — актуальное направление современного программирования. Особый интерес представляет верификация программ, написанных на распространённых языках системного программирования таких, как С. Область применения этого языка огромна: от программного обеспечения для бытовой техники до операционных систем и авионики.

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

В проекте Шармы, Дходапкара, Рамеша и др. (Bhabba Atomic Research Centre, Indian Institute of Technology) представлен метод [66] дедуктивного поиска ошибок в программах на языке MISRA С, который является индустриальным стандартом для написания безопасных программ, ориентированным в основном на встраиваемые системы. Входная С-программа моделиру-

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

Система проверки моделей для языка ANSI-C [34] описана Кларком, Кронингом и др. (Carnegie Mellon University). Заявлена поддержка большинства особенностей языка С и высокий уровень автоматизации. Для борьбы с взрывом числа состояний используется предикатная абстракция программ и парадигма CEGAR (CounterExample Guided Abstraction Refinement). Этой же группой исследователей развивается подход к использованию языка С в качестве языка спецификаций для верификации аппаратного обеспечения, описываемого на языке Verilog [35]. Дополнительный интерес представляет набор эквивалентных трансляций в языке ANSI-C, позволяющих свести задачу проверки моделей к уравнению с битовыми векторами (SAT-решатели). Кларк также участвует в разработке аналогичного проекта MAGIC (Modular Analysis of proGrams In C) [33], в котором также строится конечная модель С программ. Отметим, что верификация в данном случае имеет характер аппроксимации, поскольку циклы и рекурсия разворачиваются в некоторых границах, к тому же пользователь должен явно сформулировать эти границы.

Система С Wolf [37] (SUNY at Stone Brook, North Carolina State University) используется для извлечения конечной размеченной системы переходов из С программы. Эта модель подается на вход системе проверки моделей NCSU Concurrency Workbench. С Wolf использовался для анализа таких приложений, как GNU i-protocol и BSD ftp daemon. Отметим ряд ограничений на низкоуровневые возможности языка С, а также то, что пользователь вынужден сам моделировать механизм параллельного взаимодействия в Concurrency Workbench.

Другая система, для извлечения моделей из С программ, названная АХ (Automation extractor) и работающая в комбинации с системой проверки моделей SPIN, представлена Хольцманом (Bell Laboratories, Lucent Technologies) [45]. Предназначена система для верификации таких приложений как обеспечение телефонных АТС, распределённые операционные системы, протоколы и приложений архитектуры «клиент-сервер». Отмечалась поддержка полного языка С, но также указывалось на невозможность во многих случаях формально доказать непротиворечивость порождаемых абстракций.

Примером узкоспециализированного проекта по верификации является проект VERISOFT (University of Saarlandes, German Research Center for Artificial Intelligence) [28], ориентированного в основном на встраиваемые системы. Одна из целей проекта — верификация ядра операционной системы для простого, но верифицированного процессора. Используется очень простое подмножество языка С — язык СО, семантика которого моделируется в системе доказательства теорем Isabelle/HOL. В силу ограниченности СО в программах приходится использовать язык ассемблера, что усложняет верификацию. Вместе с тем, на языке СО были написаны верифицированные библиотеки обработки строк и списков.

Перспективный подход к верификации С программ предложен в рамках проекта Why (Франция, INRIA) [38]. Отметим, что Why — это платформа, пригодная для верификации многих императивных языков. В ней определён

одноимённый промежуточный язык, в который можно транслировать входные программы. Цель трансляции — генерация условий корректности в виде, не зависящем от системы доказательства теорем. На основе Why построен инструментарий Frama-C, предлагающий статический анализ для полного языка С и дедуктивную верификацию для ограниченного подмножества. Из ограничений отметим запреты на goto «назад» и внутрь блока, указатели на функции, приведения типов между числами и указателями, объединения, функции с переменными списками параметров, вещественные вычисления. Также с помощью языка спецификаций ACSL было аннотировано подмножество стандартной библиотеки, включающее важные функции работы с памятью и файлами. Список верифицированных программ включает довольно простые программ поиска и сортировки.

Наконец, рассмотрим проект разработки компилятора CompCert (Франция, INRI А) для языка Clight, предложенного Jlepya [32]. Этот язык представляет собой довольно большое подмножество языка С, поддерживает работу с динамической памятью (в том числе указатели на функции), объединения. Однако в выражениях Clight запрещены побочные эффекты (в частности, в выражениях запрещены операции инкремента, декремента и составного присваивания), type-декларации и оператор goto не поддерживаются. Переменные могут объявляться либо на уровне всей программы, либо в начале тела функции, т. е. это означает запрет на использование блоков. Программа на языке Clight транслируется в язык Cminor, являющийся внутренним для всей системы CompCert: в нём уменьшено число операторов и наложены дополнительные ограничения на выражения. Доказательство корректности перевода из Clight в Cminor было проведено в системе доказательства Coq и заняло 6000 строк. На выходе система генерирует ассемблерный код для процессоров PowerPC, ARM и х86, сохраняющий семантику исходного Clight кода. В сентябре 2010 года вышла версия 1.8 компилятора CompCert, которая, как заявлено на веб-сайте проекта, поддерживает оператор goto и

побочные эффекты в выражениях. Однако ссылки на печатные работы отсутствуют.

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

В лаборатории теоретического программирования ИСИ СО РАН был разработан язык С-Н^, являющийся представительным подмножеством языка С.

Формально этот язык был определён с помощью структурной операционной семантики в стиле Плоткина [59]. Хотя операционная семантика удобна для формального определения языка, для верификации она имеет слишком низкий уровень, что приводит к громоздким доказательствам условий корректности. Поэтому обычно используют аксиоматическую семантику, базирующуюся на логике Хоара [41], которая определяется как система вывода утверждений о свойствах программ. Однако аксиоматическая семантика для языка С-^М также была бы громоздкой. В связи с этим был применён двухуровневый подход: в языке С-И^ выделяется ядро — язык С-кегпе1, для которого разработана аксиоматическая семантика, и в этот язык транслируются исходные программы на языке С-Н§М. По сравнению с языком С-Н^ в языке С-кеше1 более простые выражения и более ограниченный набор операторов, что упростило аксиоматическую семантику. Стоит отметить, что использование промежуточного этапа трансляции входных программ характерно для некоторых из перечисленных выше проектов. Но трансляция осуществляется в языки, отличные от С, что ставит под вопрос её корректность. В [22] была доказана важная теорема о непротиворечивости аксиоматической

семантики языка С-кегпе1 относительно операционной, а также были описаны формальные правила перевода из языка С-Н^ в язык С-кегпе1 и дано доказательство их корректности. При верификации реальных программ (особенно среднего и большого объёма) ручной генерации условий корректности очень трудоёмкий, поэтому его целесообразно автоматизировать. Предложенная в [22] аксиоматическая семантика языка С-кегпе1 удобна для теоретических исследований, но не ориентирована на автоматическую генерацию условий корректности. Цель и задачи диссертации

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

1. Разработана новая версия операционной семантики языка С-И^.

2. Разработана смешанная аксиоматическая семантика языка С-кегпе1, позволяющая автоматически получать условия корректности и упрощать их.

3. Описан и обоснован алгоритм перевода инвариантов циклов при трансляции программ из в С-кегпе1.

4. Сформулирована и доказана теорема о корректности смешанной аксиоматической семантики языка С-кегпе1.

5. Разработан набор примеров с целью использования предложенной смешанной аксиоматической семантики С-кегпе1 для упрощения верификации.

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

В работе использовались аппараты и методы математической логики, структурного операционного подхода Плоткина, аксиоматического метода Хоара.

Научная и практическая ценность

Полученные результаты являются теоретической основной для разработки генератора условий корректности C-light программ, являющегося составной частью системы верификации СПЕКТР-2, разрабатываемой в настоящее время в лаборатории теоретического программирования ИСИ СО РАН.

Доклады и печатные работы

Основные результаты работы были представлены на конференции-конкурсе «Технологии Microsoft в теории и практике программирования» (Новосибирск, 2007 г.), VIII Всероссийской конференции молодых учёных по математическому моделированию и информационным технологиям (Новосибирск, 2007 г.), на международном семинаре «Program Understanding» (Алтай, 2009 г.), проводившемся в рамках международной конференции «Perspectives of System Informatics», международном семинаре «Program Semantics, Specif!-cation and Verification: Theory and Applications» в рамках «5 International Computer Science Symposium in Russia» (докладчик А. В. Промский), прошедшем в 2010 г. в Казани и международной Ершовской конференции по информатике PSI'l 1 (стендовый доклад, Новосибирск, 2011 г.).

Полученные результаты обсуждались на семинаре «Теоретическое и экспериментальное программирование» ИСИ СО РАН.

По материалам диссертации опубликовано 11 работ [1, 6, 7, 8, 10, 11, 15,24,29,46,47].

Структура и объём диссертации

Диссертация состоит из введения, пяти глав и заключения. Объём работы (за исключением библиографии) составляет 110 страниц в формате машинописного текста. Список литературы содержит 66 наименований. Краткое содержание работы

В главе 1 даются предварительные понятия, используемые в работе. В разд. 1.1 дано определение языка C-light. Язык C-kernel рассмотрен в разд.

1.2. Разд. 1.3 подробно описывает язык утверждений, используемый для спецификации программ, его алфавит (п. 1.3.1), выражения (п. 1.3.2) и др.

Глава 2 представляет модифицированную операционную семантику языка С-П§М. В разд. 2.1 вводится понятие абстрактной машины языка С-разд. 2.2 посвящён параметрам абстрактной машины и абстрактным функциям. В разд. 2.3 даются аксиомы и правила вывода операционной семантики С-Н^. На основе введённых в предыдущих разделах понятий в разд. 2.4 даётся определение частичной корректности. Разд. 2.5 посвящён трансляции программ из С-П^Ы в С-кегпе1: отдельно рассмотрены правила для операторов и деклараций (п. 2.5.1) и для выражений (п. 2.5.2).

В главе 3 описана смешанная аксиоматическая семантика языка С-кегпе1. В разд. 3.1 вводятся необходимые понятия. Далее подробно рассмотрены правила вывода для выражений (разд. 3.2), деклараций (разд. 3.3), операторов (разд. 3.4) и другие (разд. 3.5). Проблема перехода инвариантов циклов из в С-кегпе1 исследована в разд. 3.6.

Глава 4 полностью посвящена обоснованию корректности смешанной аксиоматической семантики относительно операционной: сформулирована и доказана теорема о непротиворечивости.

Заключительная глава 5 иллюстрирует применение смешанной операционной семантики. Рассмотрена верификация программ вычисления факториала (разд. 5.1), поиска в линейном односвязном списке (разд. 5.2) и топологической сортировки (разд. 5.3). Благодарности

Автор благодарит своего научного руководителя Валерия Александровича Непомнящего за неоценимую поддержку и внимание к работе, Игоря Сергеевича Ануреева, Алексея Владимировича Промского и Николая Вячеславовича Шилова за обсуждение и конструктивную критику работы.

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

Заключение

В рамках диссертации были получены следующие результаты:

1. Разработана новая версия операционной семантики языка

2. Разработана смешанная аксиоматическая семантика языка С-кегпе1, позволяющая автоматически получать условия корректности и упрощать их.

3. Описан и обоснован алгоритм перевода инвариантов циклов при трансляции программ из С-^Ы; в С-кегпе1.

4. Сформулирована и доказана теорема о непротиворечивости смешанной аксиоматической семантики языка С-кегпе1.

5. Разработан набор примеров с целью использования предложенной смешанной аксиоматической семантики С-кегпе1 для упрощения верификации.

В настоящее время в лаборатории теоретического программирования ведётся разработка мультиязыковой автоматизированной системы верификации СПЕКТР-2 [15, 24], которая поддерживает и язык С-%111 Предложенная в настоящей работе смешанная аксиоматическая семантика языка С-кегпе1 является основной автоматического генератора условий корректности, являющегося одним из модулей системы СПЕКТР-2.

Первые эксперименты по верификации в данной системе подтвердили полученные теоретические результаты.

Список литературы диссертационного исследования кандидат физико-математических наук Марьясов, Илья Владимирович, 2012 год

Литература

1. Ануреев И. С., Марьясов И. В., Непомнящий В. А. Верификация Сопрограмм на основе смешанной аксиоматической семантики. // Модел. и анализ информ. систем. — 2010. — Т. 17. — № 3. — С. 5 — 28. — URL: http://mais.uniyar.ac.ru/sites/default/files/journal/private/17_3_5-28.pdf.

2. Вирт Н. Алгоримы и структуры данных. — Досса: Хамарайан, 1997. — 360 с.

3. Замулин А. В. Формальные методы спецификации программ (Учебное пособие). —Новосибирск: НГУ, 1999. — 81 с.

4. Керниган Б., Ритчи Д. Язык программирования Си. — М.: Финансы и статистика, 1985.

5. Котов В. Е., Сабельфельд В. К. Теория схем программ. — М.: Наука. Гл. ред. физ.-мат. лит., 1991. — 248 с.

6. Марьясов И. В. Автоматическая верификация программ на языке C-light. // Тез. докл. VIII Всеросс. конф. молодых учёных по матем. модел. и информ. технол. — Новосибирск, 2007. — С. 103.

7. Марьясов И. В. Автоматическая верификация программ на языке C-light. // Тез. докл. конф.-конк. «Технологии Microsoft в теории и практике программирования». — Новосибирск, 2007. — С. 25 — 27.

8. Марьясов И. В. Автоматическая генерация условий корректности в системе верификации C-light программ. // Материалы XLIV Межд. научн. студ. конф. «Студент и научно-технический прогресс». — Новосибирск, 2006. —С. 253 — 254.

9. Марьясов И. В. Автоматическая генерация условий корректности для программ на языке Паскаль. // Труды XLIII Межд. научн. студ. конф. «Студент и научно-технический прогресс». — Новосибирск, 2005. — С. 181 — 186.

10. Марьясов И. В. На пути к автоматической верификации C-light программ. Смешанная аксиоматическая семантика языка C-kernel. — Ново-

сибирск, 2008. — 32 с. — (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 150). — URL: http://www.iis.nsk.Su/files/preprints/l 50.pdf.

11. Марьясов И. В. Применение смешанной аксиоматической семантики языка C-kernel к верификации программы топологической сортировки.

— Новосибирск, 2010. — 36 с. — (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 155). —URL: http://www.iis.nsk.su/files/preprints/155.pdf.

12. Непомнящий В. А. Верификация программ над массивами. // Системная информатика. —Новосибирск, 1993. —Вып. 3. — С. 68—98.

13. Непомнящий В. А. Верификация финитной итерации над наборами структур данных. // Программирование. — 2002. — № 1. — С. 3 — 12.

14. Непомнящий В. А. О проблемно-ориентированной верификации программ. // Программирование. — 1986. — №1. — С. 3 — 12.

15. Непомнящий В. А., Ануреев И. С., Атучин М. М., Марьясов И. В., Петров А. А., Промский А. В. Верификация С-программ в мультиязыковой системе СПЕКТР. // Модел. и анализ информ. систем. — 2010. — Т. 17.

— № 4. — С. 88 — 100. — URL: http://mais.uniyar.ac.ru/sites/default/files/ journal/private/17_4__88-100.pdf.

16. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С программ. Аксиоматическая семантика языка С-kernel. // Программирование. — 2003. — № 6. — С. 1 — 16.

17. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С программ. Часть 1. Язык C-light. — Новосибирск, 2001. — 48 с. — (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 84).

18. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С программ. Часть 2. Язык C-light-kernel и его аксиоматическая семантика. — Новосибирск, 2001. — 58 с. — (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 87).

19. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С программ. Часть 3. Перевод из языка C-light в

язык C-light-kernel и его формальное обоснование. — Новосибирск, 2002.

— 82 с. — (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 97).

20. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С-программ. Язык C-light. // Конф., посвященная 90-летию со дня рождения А. А. Ляпунова (пленарные доклады). — Новосибирск, 2001. — С. 423 — 432.

21. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С программ. Язык C-light и его формальная семантика. // Программирование. — 2002. — № 6. — С. 1 — 13.

22. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. Ориентированный на верификацию язык C-light. // Системная информатика: Сб. научн. труд. — Новосибирск: Изд-во СО РАН, 2004. — Вып. 9: Формальные методы и модели информатики. — С. 51 — 134.

23. Непомнящий В. А., Ануреев И. С., Промский А. В. На пути к верификации С программ. Язык C-light и его трансформационная семантика. // Problems in programming. — Kiev, 2006. — № 2 — 3. — С. 359 — 368.

24. Непомнящий В. А., Атучин М. М., Марьясов И. В., Петров А. А., Промский А. В. Система анализа и верификации С-программ СПЕКТР-2. // Труды семинара «Program Semantics, Specification and Verification». — 5th International Computer Science Symposium in Russia. — Казань, 2010. — С. 76 — 81.

25. Непомнящий В. А., Рякин О. М. Прикладные методы верификации программ. — М.: Радио и связь, 1988. — 256 с.

26. Непомнящий В. А., Сулимов А. А. Верификация программ линейной алгебры в системе СПЕКТР. // Кибернетика и системный анализ. — 1992.

— №5. —С. 136 — 144.

27. Непомнящий В. А., Сулимов А. А. Проблемно-ориентированные базы знаний и их применение в системе верификации программ СПЕКТР. //

Изв. РАН. Сер. «Теория и системы управления». — 1997. — № 2. — С. 169 — 175.

28. Alkassar Е., Hillebrand М.А., Leinenbach D., Schirmer N.W., Starostin A. The Verisoft approach to systems verification. // VSTTE 2008. — Lect. Notes Comput. Sci. — 2008. —Vol. 5295. — P. 209 — 224.

29. Anureev I., Maryasov I., Nepomniaschy V. The Mixed Axiomatic Se-mantics Method for C-program Verification. // Ershov Informatics Conference: PSI Series, 8th Edition (Preliminary Proceedings). — Novosibirsk: A. P. Ershov Institute of Informatics Systems, 2011. — P. 261 — 266.

30. Apt K. R., Olderog E. R. Verification of sequential and concurrent programs. — Springer, 1991.

31. Ball Т., Rajamani S.K. The SLAM project: debugging a system via static analysis // POPL 2002. URL: http://research.microsoft.com/en-us/projects/ slam/.

32. Blazy S., Leroy X. Mechanized semantics for the Clight subset of the С language. // Journal of Automated Reasoning. — 2009. — Vol. 43, N 3. — P. 263—288.

33. Chaki S., Clarke E. M., Groce A., Jha S., Veith H. Modular verification of software components in C. // ICSE 2003. — P. 385 — 395.

34. Clarke E. M., Kroening D., Sharygina N., Yorav K. Predicate abstraction of ANSI-C programs using SAT. // Proc. of the Model checking for dependable software-sensitive systems workshop. — San-Francisco, 2003.

35. Clarke E. M., Kroening D., Yorav K. Behavioral consistency of С and verilog programs using bounded model checking. // DAC 2003. — P.368 — 371.

36. Cousot P. Abstract interpretation based formal methods and future challenges // Lect. Notes Comput. Sci. — Berlin etc, 2001. — Vol. 2000. — P. 138 — 156.

37. Du Varney D. C., Purushothaman Iyer S. C Wolf — a toolset for extracting models from C programs. // Lect. Notes Comput. Sci. — 2002. — Vol. 2529 / 2002. —P. 260 — 275.

38. Filliâtre J.C., Marché C. Multi-prover verification of C programs // Proc. ICFEM 2004. — LNCS. — 2004. — Vol. 3308. — P. 15 — 29.

39. Floyd R. W. Assigning meanings to programs // Proc. AMS Symp. Applied Mathematics. — American Mathematical Society, Providence, R.I., 1967. — Vol. 19. —P. 19 — 31.

40. Gurevich Y., Huggins J.K. The semantics of the C programming language // Lect. Notes Comput. Sci. — Berlin etc., 1993. — Vol. 702. — P. 274 — 309.

41. Hoare C. A. R. An axiomatic basis for computer programming // Communs ACM. — 1969. — Vol. 12, N 1. — P. 576 — 580.

42. Hoare C. A. R. Assertions / Proc. of the NATO Advanced Study Inst, on Models, Algebras and Logic of Engineering Software, Marktoberdorf, Germany, July 30 — August 11, 2002. — Amsterdam, 2003. — P. 291 — 316.

43. Hoare C. A. R, Jifeng H. A trace model for pointers and objects // Lect. Notes Comput. Sci. — Berlin etc., 1999. — Vol. 1628. — P. 1 — 18.

44. Hoare C. A. R., Wirth N. An axiomatic definition of the programming language Pascal // Acta Informatica. — 1973. — Vol. 2, N 4. — P. 335 — 355.

45. Holzmann G.J. Logic verification of ANSI C code with SPIN // Lect. Notes Comput. Sci. — Berlin etc., 2000. — Vol. 1885. — P. 131 — 147.

46. Maryasov I. V. Towards automatic verification of C-light programs. Mixed

axiomatic semantics of C-kernel language. // Perspectives of Systems Infor-

tli

matics (PSI): A. Ershov 7 Int. Conf.: Int. workshop on Program Understanding. — Novosibirsk, 2009. — P. 44 — 52.

47. Maryasov I. V. The mixed axiomatic semantics method. — Novosibirsk, 2011. — 43 c. — (Preprint / RAS. Sib. branch. IIS; № 160). — http://www.iis.nsk.Su/files/preprints/l 60.pdf.

48. Moore J. S. Proving theorems about Java and the JVM with ACL2 I I Proc. of the NATO Advanced Study Inst, on Models, Algebras and Logic of Engineering Software, Marktoberdorf, Germany, July 30 — August 11, 2002. — Amsterdam, 2003. — P. 227 — 290.

49. Nepomniaschy V. A. On a symbolic method of verification for definite iteration over data structures // Joint Bulletin of the Institute of Informatics Systems and Computer Center. — 1998. — N 5. — P. 1—22.

50. Nepomniaschy V. A. Verification of pointer programs using symbolic method for definite iterations // Joint Bulletin of the Institute of Informatics Systems and Computer Center. — 2000. — N 13. — P. 56—66.

51. Nepomniaschy V. A. Symbolic verification method for definite iterations over tuples of data structures // Joint Bulletin of the Institute of Informatics Systems and Computer Center. — 2001. — N 15. — P. 103—123.

52. Nepomniaschy V. A., Anureev I. S., Promsky A. V. Verification-oriented language C-light and its structural operational semantics (extended abstract) // 5th International A. Ershov Conf. Perspectives of System Informatics (PSI 2003). — Berlin etc, 2003. — P. 103 — 111. — (Lect. Notes Comput. Sei.; 2890).

53. Nepomniaschy V. A., Sulimov A. A. Problem-oriented means of program specification and verification in project SPECTRUM // Lect. Notes Comput. Sei. — 1993. — Vol. 722. — P. 374—378.

54. Nepomniaschy V. A., Sulimov A. A. Towards Automatic Program Verification: Problem-Oriented Knowledge Bases // Specification, verification and net models of concurrent systems. — Novosibirsk, 1994. — P. 138—150.

55. Nipkow T. Hoare logics for recursive procedures and unbounded nondeterminism. — 2001. — (Draft / Fakultat fur Informatik, Technische Universität München). URL: http://www.in.tum.de/~nipkow/.

56. Norrish M. C formalised in HOL: Thes. doct. phylosophy (computer sei.). — Cambridge, 1998. — 150 p.

57. Norrish M. Derivation of verification rules for C from operational definitions // Supplementary Proc. 9th International Conf. Theorem Proving in Higher Order Logics. — TUCS General Publication N 1, Turku Centre for Computer Science, 1996. —P. 69-75.

58. Norrish M. Deterministic expressions in C // Lect. Notes Comput. Sci. — Berlin etc, 1999. —Vol. 1576. —P. 147—161.

59. Plotkin G.D. A structure approach to operational semantics. — 1981. — (Tech. Rep./ DAIMI/Aarhus University; FN-19).

60. Plotkin G.D. The origins of structural operational semantics // Inform. Processing Letters. — 2003. — Vol. 88, Issue 1-2. — P. 27—32.

61. Programming languages — C: ISO/IEC 9899:1990. — 1990.

62. Programming languages — C: ISO/IEC 9899:1999. — 1999. — 566 p.

63. Promsky A. V. Towards C-light program verification: overcoming the obstacles. // Perspectives of Systems Informatics (PSI): A. Ershov 7th Int. Conf.: Int. workshop on Program Understanding. —Novosibirsk, 2009. — P. 53 — 63.

64. Reynolds J. C. Theories of programming languages. — Cambridge University Press, 1998. — 500 p.

65. Ritchie D.M. The developement of the C language // In 2nd History of Programming Languages conf., Cambridge, Mass., — ACM, 1993.

66. Sharma B., Dhodapkar S. D., Ramesh S. Assertion checking environment (ACE) for formal verification of C programs // Lect. Notes Comput. Sci. — Berlin etc., 2002. — Vol. 2434. — P. 284—295.