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