Краткие примеры реализации абстрактной интерпретации

Question

Я прохожу курс по абстрактной интерпретации, но я не видел примеров того, как теория соотносится с реальным кодом.

Я ищу примеры короткого кода, где мне не нужно работать с целым компилятором. Анализ не должен быть полезным, я просто хотел бы увидеть пример, где анализ выводится и затем реализуется.

Кто-нибудь знает такие примеры, возможно, из университетского курса?

Answer 1

AI основан на названии математической теории Галуа Соединение. Теория очень проста:

1. Абстрактное поведение программы.
2. Выполнить анализ на абстрактном уровне.

Galois connection: для связи программ Actual и Abstract.

Это - лучший урок, который я когда-либо видел об абстрактной интерпретации:

Answer 2

Может быть, этот инструмент вам тоже интересен: Interproc Analyzer

Это абстрактный анализатор для очень простого языка, который, однако, предлагает межпроцедурный анализ. Вы можете попробовать анализ и получить числовые инварианты об анализируемой программе. Исходный код доступен (OCaml).

Действительно подробный и точный курс, прочитанный одним из «создателей» абстрактной интерпретации Патриком Кузо (уже упомянутым в одном из ответов) MIT курс об абстрактной интерпретации . Курс также предлагает задания, в OCaml.

Answer 3

Есть эта статья Бертота

Структурная абстрактная интерпретация, Формальное исследование с использованием Coq

Это дает полную реализацию абстрактного интерпретатора для простого игрушечного языкаиспользуя Coq Proof Assistant.Я использовал это для конкретной ссылки, и нашел это полезным, хотя и немного сложным, что и следовало ожидать, учитывая предмет.Coq - отличный маленький кусочек программного обеспечения.

Я также натолкнулся на статью Кузо:

Деликатное введение в формальную проверку компьютерных систем с помощью абстрактной интерпретации

грубые подробности (но я уверен, что будут полезные ссылки для полной информации) реализации в Astrée, я не знаком с Astrée, поэтому фактически не читал этот раздел, но я думаю, что он соответствует вашим критериям.

Если вы столкнетесь больше, пожалуйста, дайте мне знать!Особенно хотелось бы увидеть пролог абстрактного интерпретатора.

Answer 4

Существует MonoREIL, который поставляется с недавно открытым исходным кодом BinNavi .

См. здесь - короткое вступление.

Обратите внимание, что контекст платформы MonoREIL - это не компиляторы, а анализ двоичного кода. Тем не менее, он использовался для реальных приложений, см. Слайд 34 и далее , это введение (которое содержит более формальный фон).