http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/#notes
Комментарий от @ksromanov.
Курс Кузо — одного из основоположников абстрактной интерпретации, то есть, обобщения различных точных методов статического анализа, таких как различные методы статического анализа, основанные на monotone frameworks, статическая типизация с выводом и без вывода типов, и многих других.
Курс очень интересен широтой охвата, но страдает хаотичностью изложения. В частности, непонятно, зачем он включает теорию множеств, втиснутую в одну лекцию.
Поэтому лучше начать изучение темы с книг ниже. С другой стороны, этот курс демонстрирует подход основоположника Абстрактной интерпретации, и не совсем сразу скатывается в страницы формул в отличие от монографии Кузо Principles of Abstract Interpretation.
Комментарий от @ksromanov.
Курс, разработанный Anders Møller и др. (Aarhus University).
Конспект лекций: https://cs.au.dk/~amoeller/spa/
Обзорная лекция на youtube (часть 1): https://www.youtube.com/watch?v=Lr4cMmaJHrg
Обзорная лекция на youtube (часть 2): https://www.youtube.com/watch?v=6QQSIIvH-F0
Многими (в числе которых, скажем, John Regehr) данный специальный курс по вопросам статического анализа считается лучшим в своем роде. Мне имеет смысл только присоединиться к этому мнению. Лекции написаны очень хорошо: легкий язык, современный подход к предмету, большой охват материала.
Это превосходный курс, в который до сих пор вносятся изменения. В курсе рассказывается про разновидности статического анализа программ, базирующихся на подходе абстрактной интерпретации: вывод типов Хиндли-Милнера, Data-flow/Control-flow анализы, базирующиеся на Monotone Frameworks (частный случай абстрактной интерпретации с явным использованием решёток в качестве абстрактного домена), техника widening/narrowing. Широта охвата впечатляет.
Xavier Rival, Kwangkeun Yi. Introduction to Static Analysis An Abstract Interpretation Perspective (2020)
Комментарий от @ksromanov.
Великолепная книга, прекрасно сочетающая системность, строгость, простоту и охват. Её даже можно было бы назвать «Статический анализ программ для физиков», настолько она легко читается, не теряя достаточной строгости. Книга, по-сути, является учебником, плавно переходящим в справочник.
В первой главе авторы наглядно рассказывают об основных понятиях и методах абстрактной интерпретации на примере графического языка. В частности упоминается о тонкостях применимости соответствия Галуа. В последующих главах авторы работают с простым интерпретируемым языком, раскрывая метод построения статических анализаторов с помощью подхода абстрактной интерпретации.
После изложения теории, авторы предлагают чёткий и последовательный алгоритм создания статического анализатора, после чего демонстрируют учебный анализатор, написанный на OCaml. Заключительные главы книги уже служат скорее справочником по текущему состоянию поля.
В отличие от курса Anders'а Møller'а это не самоучитель, а учебник, к которому по-идее, должен идти задачник. Поэтому она не заменяет курс SPA, а дополняет. К сожалению, я не могу сказать, в каком порядке стоит читать эти книги. Вполне возможно, что курс SPA должен идти вторым.
С моей точки зрения, авторы используют слегка нестандартную, но очень наглядную терминологию transitional semantics (семантика малого шага) и compositional semantics (семантика большого шага), но они явно проговаривают связь с общеупотребимыми терминами. Разумеется, какие-то темы изложены явно подробнее в SPA, например оператор widening и narrowing.