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

Материал из Вики ИТ мехмата ЮФУ
Версия от 20:27, 24 августа 2009; Bravit (обсуждение | вклад) (→‎Принципы и приложения уточнённых типов (refinement types))

Перейти к: навигация, поиск
Ниже приведён список курсов лекций, прочитанных в летней школе по верификации и формальным методам «Logics and Languages for Reliability and Security», ежегодно проводимой в немецком городе Марктобердорф с 1970 года.
Ошибка создания миниатюры: /bin/bash: /usr/local/bin/convert: No such file or directory

Error code: 127
Расписание школы

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

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

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

Описанные концепции реализованные в программном анализаторе ASTRÉE, который с марта этого года является коммерчески распространяемым. Кроме статического анализа, абстрактная интерпретация может применяться для построения доказуемо корректных преобразований программ [Cousot and Cousot, 2002].

Ссылки

Многозначные автоматы и их приложения

Орна Купферман (Orna Kupferman), Еврейский университет в Иерусалиме, Израиль

Конечный автомат можно рассматривать как отображение из множества слов над алфавитом в множество {0, 1} (слово может быть принято или нет). Рассматриваются обобщения, заменяющие {0, 1} на произвольное полукольцо или решётку. К первому обобщению относится понятие взвешенного автомата. Он получается из обычного (недетерминированного) конечного автомата приписыванием переходам неотрицательных вещественных чисел (стоимости). В процессе работы автомата, стоимость переходов при чтении каждой буквы складывается. Если существует несколько вариантов работы автомата, при котором слово распознаётся, то из нескольких возможных стоимостей выбирается наименьшая; нераспознанным словам приписывается стоимость ∞(полукольцо, таким образом, образует множество неотрицательных вещественных чисел и ∞ с бинарными операциями минимума и сложения — т. н. тропическое полукольцо). Говорят, что один автомат α-аппроксимирует другой, если стоимости распознавания каждого слова отличаются не более чем в α раз. Рассматривается операция удаления переходов взвешенного автомата: говорят, что взвешенный автомат α-детерменизируем удалением переходов, если существует детерминированный автомат, который получен из исходного удалением переходов и α-аппроксимирует его.

Далее рассматриваются некоторые оптимизационные задачи: задача аренды лыж, задача замещения страниц в кэш-памяти и другие. Вводится понятие онлайн-алгоритма для решения оптимизационной задачи. Онлайн-алгоритм работает с последовательностью запросов, обработка каждого запроса имеет некоторую стоимость, особенность состоит в том, что онлайн-алгоритм не знает заранее всю последовательность запросов. Эффективность онлайн-алгоритм оценивается с помощью сравнения с оптимальным оффлайн-алгоритмом для данной оптимизационной задачи («оффлайн» означает, что вся последовательность запросов известна изначально). Это формализуется понятием α-соревновательный онлайн-алгоритм. Основная теорема этой части курса гласит, что для задачи существует α-соревновательный онлайн-алгоритм решения, если автомат, построенный по этой задаче, α-детерменизируем удалением переходов.

Вторая разновидность обобщённых автоматов предполагает, что множество состояний и отношение переходов конечного автомата являются L-множествами, где L — некоторая решётка. Обычное множество, назовём его M, можно представлять себе как отображения некоторого универсального множества в множество {0, 1} (принадлежит или не принадлежит рассматриваемому множеству M). L-множество использует тот же самый подход, но вместо {0, 1} используется решётка L. По определению в решётке есть бинарные операции ∧, ∨ — с их помощью можно определить стоимость распознавания слова. Решёточные автоматы могут использоваться для анализа решёточных линейных темпоральных логик LLTL, которые являются обобщением широко используемых в верификации ПО (а именно, в model checking) линейных темпоральных логик, LTL.

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

Ссылки

Модальные логики неподвижных точек

Герхард Ягер (Gerhard Jäger), Университет Берна, Швейцария

Ссылки

Принципы и приложения уточнённых типов (refinement types)

Эндрю Гордон (Andrew Gordon), Microsoft Research, Кэмбридж, Англия

Ссылки

Использование политик конфиденциальности (security policies) для написания безопасного (secure) ПО

Эндрю Майерс (Andrew Myers), Cornell University, США

Ссылки

Механизированные семантики

Ксавье Леруа (Xavier Leroy), INRIA, Франция

Ссылки

Эффективный анализ стохастических процессов и игр с бесконечным числом состояний

Антонин Кучера (Antonin Kučera), Masaryk University, Чехия

Ссылки

Трёхзначная абстракция и её приложения в Model Checking

Орна Грумберг (Orna Grumberg), TECHNION — Технический университет Израиля

Ссылки

Ньютоновский анализ программ

Хавьер Эспарза (Javier Esparza), Технический университет Мюнхена, Германия

Ссылки

Model Checking вычислений высших порядков

Люк Онг (Luke Ong), Оксфорд, Англия

Ссылки

Синтаксический контроль утечек и освобождения информации

Андрей Сабельфельд (Andrey Sabelfeld), Gothenburg University, Швеция

Ссылки

Два приложения систем доказательства теорем

Тобиас Нипков (Tobias Nipkow), Технический университет Мюнхена, Германия

Ссылки

Аудио некоторых лекций

Этот материал в силу своей разрозненности и неполноты не очень помогает в понимании, он выложен для того, чтобы можно было лучше представить как проходили лекции и обсуждения по итогам дня... Например, можно оценить скорость речи Гордона или понять, что Купферман единственная использовала доску и мел.

Купферман, Ягер, Сабельфельд+обсуждение, Эспарза, Кучера, Купферман, Онг+обсуждение, Нипков+обсуждение, Леруа, Гордон, Грумберг.

Источник — «http://it.mmcs.sfedu.ru/_wiki/index.php?title=Летняя_школа_в_г._Марктобердорф_2009&oldid=3047»