Верификация компиляторов – систематический подход.

Верификация компиляторов – систематический подход.

С.В. Зеленов, Н.В. Пакулин.

Аннотация

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

Издание

Труды Института системного программирования РАН, том 13, часть 1, 2007, стр. 47-64.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

Для цитирования

С.В. Зеленов, Н.В. Пакулин. Верификация компиляторов – систематический подход.. Труды Института системного программирования РАН, том 13, часть 1, 2007, стр. 47-64. .

Полный текст статьи в формате pdf Вернуться к содержанию тома