Летняя школа в г. Марктобердорф 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 and Cousot, 2002].
Ссылки
- Аннотация лектора
- Basic Concepts of Abstract Interpretation
- Abstract interpretation based static analysis parameterized by semantics
- Abstract interpretation of resolution-based semantics
- A Case Study in Abstract Interpretation Based Program Transformation: Blocking Command Elimination
- Automatic Verification by Abstract Interpretation
- Constructive design of a hierarchy of semantics of a transition system by abstract interpretation
Многозначные автоматы и их приложения
Орна Купферман (Orna Kupferman), Еврейский университет в Иерусалиме, Израиль.
Конечный автомат можно рассматривать как отображение из множества слов над алфавитом в множество {0, 1} (слово может быть принято или нет). Рассматриваются обобщения, заменяющие {0, 1} на произвольное полукольцо или решётку. К первому обобщению относится понятие взвешенного автомата. Он получается из обычного (недетерминированного) конечного автомата приписыванием переходам неотрицательных вещественных чисел (стоимости). В процессе работы автомата, стоимость переходов при чтении каждой буквы складывается. Если существует несколько вариантов работы автомата, при котором слово распознаётся, то из нескольких возможных стоимостей выбирается наименьшая; нераспознанным словам приписывается стоимость ∞(полукольцо, таким образом, образует множество неотрицательных вещественных чисел и ∞ с бинарными операциями минимума и сложения — т. н. тропическое полукольцо). Говорят, что один автомат α-аппроксимирует другой, если стоимости распознавания каждого слова отличаются не более чем в α раз. Рассматривается операция удаления переходов взвешенного автомата: говорят, что взвешенный автомат α-детерменизируем удалением переходов, если существует детерминированный автомат, который получен из исходного удалением переходов и α-аппроксимирует его.
Далее рассматриваются некоторые оптимизационные задачи: задача аренды лыж, задача замещения страниц в кэш-мапяти и другие. Вводится понятие онлайн-алгоритма для решения оптимизационной задачи. Онлайн-алгоритм работает с последовательностью запросов, обработка каждого запроса имеет некоторую стоимость, особенность состоит в том, что онлайн-алгоритм не знает заранее всю последовательность запросов. Эффективность онлайн-алгоритм оценивается с помощью сравнения с оптимальным оффлайн-алгоритмом для данной оптимизационной задачи («оффлайн» означает, что вся последовательность запросов известна изначально). Это формализуется понятием α-соревновательный онлайн-алгоритм. Основная теорема этой части курса гласит, что для задачи существует α-соревновательный онлайн-алгоритм решения, если автомат, построенный по этой задаче, α-детерменизируем удалением переходов.
Вторая разновидность обобщённых автоматов предполагает, что множество состояний и отношение переходов конечного автомата являются L-множествами, где L — некоторая решётка. Обычное множество, назовём его M, можно представлять себе как отображения некоторого универсального множества в множество {0, 1} (принадлежит или не принадлежит рассматриваемому множеству M). L-множество использует тот же самый подход, но вместо {0, 1} используется решётка L. По определению в решётке есть бинарные операции ∧, ∨ — с их помощью можно определить стоимость распознавания слова. Решёточные автоматы могут использоваться для анализа решёточных линейных темпоральных логик LLTL, которые являются обобщением широко используемых в верификации ПО (а именно, в model checking) линейных темпоральных логик, LTL.
В курсе приведены оценки сложности операций, связанных с понятиями аппроксимации, вложения, детерминируемости удалением переходов многозначных автоматов и др.
