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

Question

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

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

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

Answer 1

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

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

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

Answer 2

AI основана на математической теории имени Galois Connection. Теория очень проста:

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

Galois connection: Чтобы связать Actual а также Abstract программа.

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

Answer 3

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

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

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

Я также сталкивался в газете Cousot:

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

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

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

Answer 4

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

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

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