Летняя школа в г. Марктобердорф 2009

Ниже приведён список курсов лекций, прочитанных в летней школе по верификации и формальным методам «Logics and Languages for Reliability and Security», ежегодно проводимой в немецком городе Марктобердорф с 1970 года.

Анализ и верификация программ с помощью абстрактной интерпретации

Патрик Кюзо (Patrick Cousot), École Normale Supérieure, Париж, Франция.

В исследованиях по верификации программ самой популярной моделью для программы является система переходов: тройка из множества состояний, его подмножества начальных состояний и бинарного отношения перехода на множестве состояний, которое является отношением порядка. Можно рассмотреть иерархию семантик программ, абстрагированных таким образом. Например, множество цепей, порождённых отношением перехода называют семантикой частичных трасс (partial trace semantics). Эту семантику можно абстрагировать, оставив от каждой цепи её начало и конец — получается семантика рефлексивного транзитивного замыкания отношения перехода. Вводятся несколько подобных семантик, которые выстраиваются в иерархию в том смысле, что определяются операторы абстрагирования и конкретизации, позволяющие переходить между уровнями этой иерархии (различными семантиками). Каждая пара операторов абстрагирования—конкретизации, как правило, обладают связью Галуа (Galois connection). Каждая из рассматриваемых семантик может быть определена в форме неподвижной точки специального оператора, что позволяет проводить вычисления этих семантик — с помощью теоремы Клини, используя итерации Клини. Сложность состоит в том, что в конкретных случаях итерации Клини могут расходиться (неподвижная точка, хотя в силу теоремы Клини существует, но не достигается). Для уточнения процесса поиска неподвижных точек понятия операторов расширения (widening) и сужения (narrowing), которые подбираются в каждом случае отдельно.

Описанные концепции реализованные в программном анализаторе ASTRÉE, который с марта этого года является коммерчески распространяемым.

Ссылки

• Cousot. Basic Concepts of Abstract Interpretation
• Cousot. Abstract interpretation based static analysis parameterized by semantics
• Cousot. Abstract interpretation of resolution-based semantics
• A Case Study in Abstract Interpretation Based Program Transformation: Blocking Command Elimination
• Cousot. Automatic Verification by Abstract Interpretation
• Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation