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