В работе представлен систематический подход
В работе представлен систематический подход к верификации компиляторов. Общая задача верификации компилятора декомпозирована на подзадачи верификации отдельных аспектов функциональности компилятора. Декомпозиция задачи верификации позволяет начинать верификацию на ранних этапах создания компилятора и проводить её параллельно разработке. Тем самым, сокращается продолжительность цикла разработки компилятора и снижаются суммарные затраты на тестирование компилятора. Для всех выделенных подзадач предложены методы верификации, построенные в рамках единого подхода тестирования на основе формальных спецификации и моделей. Для всех методов существуют их подробные описания и инструментальная поддержка для их практического применения. Представленный подход использовался при тестировании компиляторов Си и Java, а также трансляторов расширений языков программирования, разработанных в ИСП РАН [].
