Летняя школа в г. Марктобердорф 2009 — различия между версиями

Материал из Вики ИТ мехмата ЮФУ
Перейти к: навигация, поиск
(→‎Ньютоновский анализ программ)
(→‎Ссылки)
Строка 67: Строка 67:
 
===Ссылки===
 
===Ссылки===
 
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Esparza_Abs_09.pdf Аннотация автора]
 
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Esparza_Abs_09.pdf Аннотация автора]
−
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Esparza.%20newtProgAn.pdf Newtonian Program Analysis]
+
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Esparsa/Esparza.%20newtProgAn.pdf Newtonian Program Analysis]
 +
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Esparsa/Kuich.%20Omega-cont.%20semirings,%20algebraic%20systems%20and%20PDA.pdf Kuich. Omega-cont. semirings, algebraic systems and PDA]
  
 
==Принципы и приложения уточнённых типов (refinement types)==
 
==Принципы и приложения уточнённых типов (refinement types)==

Версия 18:04, 23 сентября 2009

Ниже приведён список курсов лекций, прочитанных в летней школе по верификации и формальным методам «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), Университет Берна, Швейцария

В первой части курса последовательно рассматриваются синтаксис, семантика и различные аксиоматизации µ-исчисления. µ-исчисление расширяет обычное исчисление высказываний[1] операторами наименьшей и наибольшей неподвижных точек, которые широко используются при изучении систем переходов (в курсе приводились примеры выражения свойств живучести и безопасности системы на языке неподвижных точек). При изучении помеченных систем переходов, когда есть не одно отношение перехода, а целое семейство этих отношений, подходящую формализацию доставляет добавление в логику модальностей. Семантика модального µ-исчисления вводится с помощью систем переходов (например, пропозициональным переменным ставятся в соответствие множества состояний системы, в которых они считаются истинными). Наиболее очевидная аксиоматизация µ-исчисления, хотя обладает обоими фундаментальными свойствами формальных исчислений в отношении семантики, полнотой и корректностью (soundness) (то есть, грубо говоря, все истинные в данной семантике утверждения могут быть доказаны и только они), является неудобной для автоматического поиска доказательств — в основном из-за присутствия правила Modus Ponens (MP). В связи с этим развивается семантика µ-исчисления: доказывается разрешимость задачи выполнимости формулы (однако лучший теоретико-сложностный результат для этой задачи NP ∩ coNP — интересно, имеется ли полиномиальный алгоритм) и теорема о малой модели, которая говорит, что если формула выполняется на какой-то системе переходов, то она выполняется на некоторой конечной (экспоненциально большой от размера формулы) системе переходов. Последнее позволяет выполнить следующий трюк. Строится полная и корректная аксиоматиация µ-исчисления, свободная от MP (говорят: «свободная от сечений»), но содержащая одно правило вывода с бесконечным (счётным) количеством посылок (которые являются итерациями оператора наибольшей неподвижной точки), а затем с помощью теоремы о малой модели доказывается, что любой вывод в этой аксиоматизации можно оборвать после конечного числа шагов — это позволяет сформулировать финитарный вариант аксиоматизации µ-исчисления, который также (доказывается) является полным и корректным. Открытыми остаются вопросы о том, можно ли получить финитарную аксиоматизацию на основе рассмотренных, не прибегая к семантическим доводам (чисто синтаксическими методами), и есть ли более естественный путь построения свободной от сечений аксиоматизации µ-исчисления.

Во второй части курса изучаются различные сужения µ-исчисления для формализации понятия знания и общего знания. Если ограничиться рассмотрением систем переходов, семейство отношений перехода которых представляет собой конечное множество, то пронумеровав его элементы, можно смотреть на него как на набор стратегий n агентов. Формулы с модальностями трактуются в стиле эпистемологической логики: [a]ψ понимается как «a знает, что ψ» (a ∊ {1,..,n}). Для выражения общего знания достаточно ограничиться применением операторов неподвижной точки к формулам специального вида — мы получаем подсистему модального µ-исчисления, которая остаётся полной и корректной. Полностью избавиться от сечений не удаётся и здесь, однако имеется следующий результат: для истинного множества формул Г можно заранее указать множество формул DC(Г), которые будут использоваться в сечениях при выводе этих формул — мы получаем некий контроль над сечениями. DC(Г) является специфическим дизъюнктивно-конъюнктивным замыканием Г, которое, однако, всё ещё слишком велико, чтобы приносить пользу на практике. Есть ощущение, что его можно сузить — это является одним из открытых вопросов.

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

Ссылки

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

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

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

Занимаясь межпроцедурным анализом программ можно поступить так: пусть есть несколько процедур, вызывающих друг друга, тогда, выписывая выражение указанным выше образом для каждой, можно инструкцию вызова другой процедуры заменять именем этой процедуры, понимая его как имя переменной. В результате получается система алгебраических уравнений нескольких переменных. Важная информация о поведении программы может быть получена из решения этой системы. Характер информации зависит, конечно, от того, какой смысл вложен в операции полукольца. В частности, можно подсчитывать вероятности завершения программы или наименьшее количество выполнений фрагментов программы перед завершением. Более того, уравнения такого вида могут анализироваться в контексте задач, несвязанных с анализом программ: например, если рассматривать полукольцо языков, состоящих из слов над некоторым алфавитом, то система алгебраических уравнений задаёт контекстно-свободную грамматику, а её наименьшее решение является языком этой грамматики.

Первые методы решения систем алгебраических уравнений над данным полукольцом основывались на вариантах теоремы Клини о неподвижной точке для решёток: на полукольце вводится частичный порядок, связанный с полукольцевыми операциями, алгебраические функции автоматически являются непрерывными и монотонными, чего требует классическая теорема Клини. Метод Клини для нахождения наименьшей неподвижной точки отображения (который даёт теорема Клини) имеет ряд недостатков: он может не давать значения неподвижной точки (и так происходит в ряде важных случаев, например, при решении некоторых уравнений, содержащих операцию * — звезду Клини), он может сходиться к неподвижной точке очень медленно. Для решения этих проблем итерационный метод Ньютона был распространён на ω-непрерывные полукольца. Имеется две очевидных сложности на этом пути: отсутствия вычитания и деления. Деление используется в определении производной, однако производную полинома можно определить формально, используя фигурирующие в анализе формулы для производной произведения и суммы. Разность же (например, a-b) может быть заменена элементом (например, c) с соответствующим свойством(c+b=a) — доказывается, что такой элемент существует и, что, каким бы его ни выбрать, будет получено одно и то же приближение на очередной итерации метода Ньютона.

Кроме информации, полученной с решением системы, интерес могут представлять приближения, вычисляемые на каждой итерации. Например, для упомянутого выше полукольца языков i-ое приближение описывает подмножество слов языка данной грамматики индекса i (слово имеет индекс i, если существует вывод этого слова, такой что в каждой сентенциальной форме участвует не более, чем i нетерминалов); кроме того, приближения Клини и Ньютона можно охарактеризовать также с помощью свойств деревьев вывода для слов, содержащихся в них.

Ссылки

Принципы и приложения уточнённых типов (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 — Технический университет Израиля

Ссылки

Ссылки

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

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

Ссылки

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

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

Ссылки

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

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

Ссылки

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

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

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

Примечания

  1. ↑ Не рекомендуется консультироваться со статьёй об исчислении высказываний в русской Википедии.
Источник — «http://it.mmcs.sfedu.ru/_wiki/index.php?title=Летняя_школа_в_г._Марктобердорф_2009&oldid=3166»