Просмотр исходного текста страницы Летняя школа в г. Марктобердорф 2009

Ниже приведён список курсов лекций, прочитанных в летней школе по верификации и формальным методам «[http://asimod.in.tum.de/ Logics and Languages for Reliability and Security]», ежегодно проводимой в немецком городе Марктобердорф с 1970 года. [[Image:Timetable-Marktoberdorf09.jpg|thumb|right|Расписание школы]]

==Анализ и верификация программ с помощью абстрактной интерпретации==
'''Патрик Кюзо ([http://www.di.ens.fr/~cousot/ Patrick Cousot]), École Normale Supérieure, Париж, Франция'''

В исследованиях по верификации программ самой популярной моделью для программы является ''система переходов'': тройка из множества состояний, его подмножества начальных состояний и бинарного отношения перехода на множестве состояний, которое является отношением порядка. Можно рассмотреть иерархию семантик программ, абстрагированных таким образом. Например, множество [http://en.wikipedia.org/wiki/Total_order#Chains цепей], порождённых отношением перехода называют ''семантикой частичных трасс'' (partial trace semantics). Эту семантику можно абстрагировать, оставив от каждой цепи её начало и конец — получается ''семантика рефлексивного транзитивного замыкания'' отношения перехода. Вводятся несколько подобных семантик, которые выстраиваются в иерархию в том смысле, что определяются операторы абстрагирования и конкретизации, позволяющие переходить между уровнями этой иерархии (различными семантиками). Каждая пара операторов абстрагирования—конкретизации, как правило, обладают связью Галуа ([http://en.wikipedia.org/wiki/Galois_connection Galois connection]). Каждая из рассматриваемых семантик может быть определена в форме неподвижной точки специального оператора, что позволяет проводить вычисления этих семантик — с помощью [http://en.wikipedia.org/wiki/Kleene_fixpoint_theorem теоремы Клини], используя итерации Клини. Сложность состоит в том, что в конкретных случаях итерации Клини могут расходиться (неподвижная точка, хотя в силу теоремы Клини существует, но не достигается). Для уточнения процесса поиска неподвижных точек понятия операторов расширения (widening) и сужения (narrowing), которые подбираются в каждом случае отдельно.

Описанные концепции реализованные в программном анализаторе [http://www.astree.ens.fr/ ASTRÉE], который с марта этого года является коммерчески распространяемым. Кроме статического анализа, абстрактная интерпретация может применяться для построения доказуемо корректных преобразований программ [[http://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-02-ACM-p178--190-2002-A4.ps.gz Cousot and Cousot, 2002]].

===Ссылки===
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Cousot_Abs_09.pdf Аннотация лектора]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20Basic%20Concepts%20of%20Abstract%20Interpretation.pdf Basic Concepts of Abstract Interpretation]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20Abstract%20interpretation%20based%20static%20analysis%20parameterized%20by%20semantics%20.pdf Abstract interpretation based static analysis parameterized by semantics]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20Abstract%20interpretation%20of%20resolution-based%20semantics.pdf Abstract interpretation of resolution-based semantics]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20A%20Case%20Study%20in%20Abstract%20Interpretation%20Based%20Program%20Transformation_%20Blocking%20Command%20Elimination.pdf A Case Study in Abstract Interpretation Based Program Transformation: Blocking Command Elimination]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20Automatic%20Verification%20by%20Abstract%20Interpretation.pdf Automatic Verification by Abstract Interpretation]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Cousot/Cousot.%20Constructive%20design%20of%20a%20hierarchy%20of%20semantics%20of%20a%20transition%20system%20by%20abstract%20interpretation.pdf Constructive design of a hierarchy of semantics of a transition system by abstract interpretation]

==Многозначные автоматы и их приложения==
'''Орна Купферман ([http://www.cs.huji.ac.il/~ornak/ Orna Kupferman]), Еврейский университет в Иерусалиме, Израиль'''

[http://ru.wikipedia.org/wiki/Конечный_автомат Конечный автомат] можно рассматривать как отображение из множества слов над алфавитом в множество {0, 1} (слово может быть принято или нет). Рассматриваются обобщения, заменяющие {0, 1} на произвольное [http://en.wikipedia.org/wiki/Semiring полукольцо] или [http://ru.wikipedia.org/wiki/Решётка_(теория_множеств) решётку]. К первому обобщению относится понятие взвешенного автомата. Он получается из обычного (недетерминированного) конечного автомата приписыванием переходам неотрицательных вещественных чисел (стоимости). В процессе работы автомата, стоимость переходов при чтении каждой буквы складывается. Если существует несколько вариантов работы автомата, при котором слово распознаётся, то из нескольких возможных стоимостей выбирается наименьшая; нераспознанным словам приписывается стоимость ∞(полукольцо, таким образом, образует множество неотрицательных вещественных чисел и ∞ с бинарными операциями минимума и сложения — т. н. [http://en.wikipedia.org/wiki/Tropical_semiring#Basic_definitions тропическое полукольцо]). Говорят, что один автомат α-аппроксимирует другой, если стоимости распознавания каждого слова отличаются не более чем в α раз. Рассматривается операция удаления переходов взвешенного автомата: говорят, что взвешенный автомат α-детерменизируем удалением переходов, если существует детерминированный автомат, который получен из исходного удалением переходов и α-аппроксимирует его.

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

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

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

===Ссылки===
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Kupferman_Abs_09.pdf Аннотация лектора]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Kupferman/Kupferman%20et%20al.%20Reasoning%20about%20Online%20Algorithms%20with%20Weighted%20Automata.pdf Reasoning about Online Algorithms with Weighted Automata]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Kupferman/Kupferman,%20Lustig.%20Lattice%20Automata.pdf Lattice Automata]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Kupferman/Albers.%20Competitive%20Online%20Algorithms,%201996.ps Albers. Competitive Online Algorithms]
*[http://springerlink.com/content/x4432l/?p=dfe6eec16d6344e7a65f63d1786e1e4b&pi=0 Handbook of Weighted Automata // Monographs in Theoretical Computer Science, Springer-Verlag, 2009.]

==Модальные логики неподвижных точек==
'''Герхард Ягер ([http://www.iam.unibe.ch/til/staff/jaeger Gerhard Jäger]), Университет Берна, Швейцария'''

В первой части курса последовательно рассматриваются синтаксис, семантика и различные аксиоматизации µ-исчисления. µ-исчисление расширяет обычное [http://en.wikipedia.org/wiki/Propositional_calculus исчисление высказываний]<ref>Не рекомендуется консультироваться со статьёй об исчислении высказываний в русской Википедии.</ref> операторами наименьшей и наибольшей неподвижных точек, которые широко используются при изучении [http://en.wikipedia.org/wiki/Transition_system систем переходов] (в курсе приводились примеры выражения свойств живучести и безопасности системы на языке неподвижных точек). При изучении ''помеченных'' систем переходов, когда есть не одно отношение перехода, а целое семейство этих отношений, подходящую формализацию доставляет добавление в логику [http://en.wikipedia.org/wiki/Modal_logic модальностей]. Семантика модального µ-исчисления вводится с помощью систем переходов (например, пропозициональным переменным ставятся в соответствие множества состояний системы, в которых они считаются истинными). Наиболее очевидная аксиоматизация µ-исчисления, хотя обладает обоими фундаментальными свойствами формальных исчислений в отношении семантики, полнотой и корректностью (soundness) (то есть, грубо говоря, все истинные в данной семантике утверждения могут быть доказаны и только они), является неудобной для автоматического поиска доказательств — в основном из-за присутствия правила [http://ru.wikipedia.org/wiki/Modus_ponens Modus Ponens] (MP). В связи с этим развивается семантика µ-исчисления: доказывается разрешимость задачи выполнимости формулы (однако лучший теоретико-сложностный результат для этой задачи NP ∩ coNP — интересно, имеется ли полиномиальный алгоритм) и теорема о малой модели, которая говорит, что если формула выполняется на какой-то системе переходов, то она выполняется на некоторой конечной (экспоненциально большой от размера формулы) системе переходов. Последнее позволяет выполнить следующий трюк. Строится полная и корректная аксиоматиация µ-исчисления, свободная от MP (говорят: «свободная от сечений»), но содержащая одно правило вывода с бесконечным (счётным) количеством посылок (которые являются итерациями оператора наибольшей неподвижной точки), а затем с помощью теоремы о малой модели доказывается, что любой вывод в этой аксиоматизации можно оборвать после конечного числа шагов — это позволяет сформулировать финитарный вариант аксиоматизации µ-исчисления, который также (доказывается) является полным и корректным. Открытыми остаются вопросы о том, можно ли получить финитарную аксиоматизацию на основе рассмотренных, не прибегая к семантическим доводам (чисто синтаксическими методами), и есть ли более естественный путь построения свободной от сечений аксиоматизации µ-исчисления.

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

В заключении курса приведён пример исчисления, соединяющего в себе суженное модальное µ-исчисление для n агентов и «логику доказательств», разработанную [http://web.cs.gc.cuny.edu/~sartemov/ Сергеем Артёмовым]. Последняя рассматривает понятие «свидетельства доказательства», когда в процессе вывода формул к ним приписываются по определённым правилам специальные термы («свидетельства»). Обнаружено несколько интересных соотношений между понятиями свидетельства, знания и общего знания, однако это направление требует дальнейшей разработки.

===Ссылки===
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Jaeger_Abs_09.pdf Аннотация лектора]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Bradfield,%20Stirling.%20Modal%20Mu-Calculi.pdf Bradfield, Stirling. Modal Mu-Calculi]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/About%20cut%20elimination%20for%20logics%20of%20common%20knowledge.pdf About cut elimination for logics of common knowledge]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Cut-free%20common%20knowledge.pdf Cut-free common knowledge]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Brunnler,%20Studer.%20Syntactic%20Cut-elimination%20for%20Common%20Knowledge.pdf Brunnler, Studer. Syntactic Cut-elimination for Common Knowledge]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Yavorskaya.%20Interacting%20Explicit%20Evidence%20Systems.pdf Yavorskaya. Interacting Explicit Evidence Systems]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Artemov.%20Evidence-based%20common%20knowledge.pdf Artemov. Evidence-based common knowledge]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Artemov,%20Beklemishev.%20Provability%20logic.pdf Artemov, Beklemishev. Provability logic]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Jager/Walukiewicz.%20How%20to%20Fix%20It_%20Using%20Fixpoints%20in%20Different%20Contexts%20.pdf Walukiewicz. How to Fix It_ Using Fixpoints in Different Contexts]

==Ньютоновский анализ программ==
'''Хавьер Эспарза ([http://www7.informatik.tu-muenchen.de/~esparza/ Javier Esparza]), Технический университет Мюнхена, Германия'''

Ряд методик анализа программ основывается на изучении управляющего графа программы. Один распространённый подход к анализу потока данных программы основывается на приписывании каждой инструкции программы значения из некоторой [http://en.wikipedia.org/wiki/Semilattice полурешётки] и введении в этой решётке операции «произведения», соответствующей конкатенации (последовательному выполнению) инструкций, которое (после некоторых дополнительных усилий) превращает исходную полурешётку в идемпотентное [http://en.wikipedia.org/wiki/Semiring полукольцо]. В терминах управляющего графа программы это означает приписывание дугам значений полукольца. Последовательный фрагмент программы можно записать как произведение таких значений, а фрагмент с ветвлениями — как сложение. В результате фрагмент программы может быть выражен алгебраически. 

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

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

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

===Ссылки===
*[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/Esparsa/Esparza.%20newtProgAn.pdf Newtonian Program Analysis]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Esparsa/Kuich.%20Semirings%20and%20FPS.pdf Kuich. Semirings and Formal Power Series]

==Принципы и приложения уточнённых типов (refinement types)==
'''Эндрю Гордон ([http://research.microsoft.com/en-us/um/people/adg/ Andrew Gordon]), Microsoft Research, Кэмбридж, Англия'''

Курс лекций состоял из трёх частей, в каждой из которых рассматривались технологии (языки программирования, моделирования и формальные языки), решающие задачи, связанные с безопасностью (в разных смыслах этого слова). Общий подход к решению задачи доказательства некоторых свойств системы таков: разработать достаточно богатую для выражения интересующего свойства систему типов и попытаться оттипизировать исследуемую систему. На этом пути важным инструментом являются уточнённые типы. Идея уточнённых типов проста: уточнённый тип это базовый тип плюс предикат для значения этого типа. Например, уточнённый тип чётных чисел это целые числа плюс предикат проверки на чётность. Использование этой идеи в промышленном программировании многие годы сдерживалось разными факторами: проверка предикатов была не достаточно эффективна, не всегда возможна и не всегда надёжна. Последние достижения в разработке формальных методов, появление эффективных инструментов класса [http://en.wikipedia.org/wiki/SMT_solver SMT solvers] и появление задач, в которых некоторые недостатки реализации уточнённых типов не играют решающей роли, изменили положение дел.

Первая часть знакомила с [http://msdn.microsoft.com/en-us/oslo/default.aspx проектом «Oslo»] от Microsoft. Oslo это набор технологий для моделирования жизненного цикла и характеристик корпоративных приложений, разрабатываемых с использованием разнообразных технологий Microsoft (.NET, ASP.NET, Visua Studio, XAML). Такое моделирование предусматривает высокоуровневое описание форматов данных, схем данных, окружений и источников данных. Это новая ступень эволюции таких известных средств как, например, конфигурационные файлы, управляющие сценарии, XML-[http://en.wikipedia.org/wiki/Deployment_Descriptor дескрипторы развёртывания] корпоративных приложений. 

Составной частью проекта Oslo является [http://msdn.microsoft.com/en-us/library/dd129617%28VS.85%29.aspx язык M]. Были продемонстрированы детали реализации уточнённых типов в этом языке и приведён пример описания некоторой политики безопасности для приложений (обычно описываемой в XML-файлах и диктующей, к примеру, использование криптоключей определённой длины, сертификатов и т. п.) с помощью системы типов M: в конечном счёте определяется тип «безопасная конфигурация», и конкретные конфигурации приложений могут быть пропущены через type checker и допущены или отвергнуты. Более подробное описание достоинств системы типов M содержится в ещё не опубликованной работе Bierman, Gordon, Langworthy.

Вторая часть курса посвящена описанию подхода к верификации криптопротоколов на основе верификации программного кода этих протоколов, выполненных на функциональном языке с поддержкой конкурентности (concurrency) в духе [http://en.wikipedia.org/wiki/Pi-calculus pi-исчисления] — [http://en.wikipedia.org/wiki/F_Sharp_%28programming_language%29 F#]. В третьей части курса рассматривается новая формальная система RFC (Refined Concurrent FPC (Fixpoint Calculus); FPC — возможная формальная основа ML и Haskell, разработанная Плоткиным, 1985 и Гюнтером, 1992), которая должна служить теоретическим базисом для полноценной реализации идей, встретившихся во второй части. Кроме FPC, pi-calculus и уточнённых типов используются такие теоретические разработки как печати Морриса (см. ссылки), спецификации безопасности assume/assert (Флойд, Хоар, Дейкстра) и другие. Описывается разрабатывающийся в настоящее время язык F7, расширение F#, который должен стать реализацией RFC. С помощью богатых выразительных средств F7 можно описывать требования безопасности в виде интерфейсов, а затем проверять соответствие этим интерфейсам реализаций криптопротоколов на F# (такая проверка типов является частью F7).

===Ссылки===
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Gordon_Abs_09.pdf Аннотация автора]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Gordon/Principles%20and%20Applications%20of%20Refinement%20Types,%20slides.pdf Слайды]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Gordon/refinement-types-for-secure-implementations.pdf Refinement Types for Secure Implementations]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Gordon/morris73.pdf Morris, Protection in Programming Languages]

==Model Checking вычислений высших порядков==
'''Люк Онг ([http://users.comlab.ox.ac.uk/luke.ong/ Luke Ong]), Оксфорд, Англия'''

Зарекомендовавшим себя формализмом для представления программ на функциональных языках программирования (использующих [http://ru.wikipedia.org/wiki/Функция_высшего_порядка вычисления высших порядков]) являются ''схемы рекурсии высших порядков'': это синтаксический инструмент наподобие порождающих [http://ru.wikipedia.org/wiki/Формальная_грамматика грамматик Хомского], описывающий (бесконечные) деревья (слова, описываемые грамматиками Хомского, являются, очевидно, частным случаем деревьев). Схемы рекурсии могут также рассматриваться как уравнения, записанные в термах, принадлежащих фрагменту [http://en.wikipedia.org/wiki/Simply-typed_lambda_calculus просто типизированного λ-исчисления]. Позволяя конечными средствами описывать бесконечный объект, схемы рекурсии являются актуальным понятием в приложениях к верификации ПО, а именно software model cheking (в отличие от уже достаточно разработанного hardware model cheking, работающего с системами с конечным числом состояний). В первой части курса устанавливается связь между схемами рекурсии и стековыми автоматами высших порядков (САВП). Последние были введены ещё А. Н. Масловым в 74 году и являются обобщением обычных [http://ru.wikipedia.org/wiki/Стековый_автомат стековых автоматов], у которых внутри стека хранятся другие стеки, внутри которых хранятся другие стеки и т. д., глубиной вложенности ''n'' для ''стекового автомата порядка n''. Приводятся примеры описания одних и тех же языков с помощью схем рекурсии и САВП. Основной результат, существовавший до недавнего времени это равномощность САВП и ''сохранных'' (safe) схем рекурсии. Совсем недавно была доказана эквивалентность общих схем рекурсии и ''сворачивающихся'' (collapsible) САВП. Последние представляют собой САВП с возможностью в любой момент развернуть стек до определённого (заранее отмеченного) места. Тем не менее, являются ли ССАВП собственным подклассом САВП, остаётся открытым вопросом. Множество открытых вопросов остаётся также в отношении «''иерархии Маслова''» языков САВП (например, 0-языки это регулярные языки, 1-языки это контекстно-свободные языки, 2-языки это [http://en.wikipedia.org/wiki/Indexed_language индексированные языки], предложенные Ахо в 68 году, строго более широкие, чем КС-языки — являются ли 3-языки в точности контекстно-зависимыми языками? можно ли предложить для языков САВП аналоги [http://ru.wikipedia.org/wiki/Лемма_о_накачке лемм о накачке]?). При описании семантики и верификации ПО, использующего вычисления высших порядков удобно иметь в запасе оба рассмотренных формализма.

Далее в курсе формулируется задача Model Checking для вычислений высших порядков. Модели задаются деревьями, порождаемыми схемами рекурсии или играми. Для спецификации используются формулы [http://en.wikipedia.org/wiki/Monadic_second-order_logic монадических теорий второго порядка теорий] (МВП-теорий) (которые, как утверждается, дают золотую середину выразительности для выражения необходимых свойств системы). Приводятся новые результаты о разрешимости МВП-теорий (и её сложности). Рассматривается метод решения задачи Model Checking, основанный на сведении её к задаче типизации исходной схемы рекурсии.

===Ссылки===
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Ong_Abs_09.pdf Аннотация автора]
*Слайды к лекциям: [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/slides-part1.pdf  часть 1], [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/slides-part2.pdf часть 2]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Ong.%20On%20model-checking%20trees%20generating%20by%20higher-order%20recursion%20schemes,%202006.pdf Ong et al. On model-checking trees generating by higher-order recursion schemes, 2006]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Ong%20et%20al.%20Collapsible%20Pushdown%20Automata%20and%20Recursion%20Schemes,%202008.pdf Ong et al. Collapsible Pushdown Automata and Recursion Schemes, 2008]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Hague,%20Ong.%20Symbolic%20Backwards-Reachability%20Analysis%20for%20Higher-Order%20Pushdown%20Systems,%202008.pdf Hague, Ong. Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems, 2008]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Knapik%20et%20al.%20Deciding%20Monadic%20Theories%20of%20Hyperalgebraic%20Trees,%202001.pdf Knapik et al. Deciding Monadic Theories of Hyperalgebraic Trees, 2001]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Knapik%20et%20al.%20Higher-Order%20Pushdown%20Trees%20Are%20Easy,%202002.pdf Knapik et al. Higher-Order Pushdown Trees Are Easy, 2002]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Knapik%20et%20al.%20Unsafe%20Grammars%20and%20Panic%20Automata,%202005.pdf Knapik et al. Unsafe Grammars and Panic Automata, 2005]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Blum,%20Ong.%20The%20Safe%20Lambda%20Calculus,%202009,%20LMCS.pdf Blum, Ong. The Safe Lambda Calculus, 2009, LMCS]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/de%20Miranda.%20Structures%20Generated%20by%20Higher-Order%20Grammars%20and%20the%20Safety%20Constraint,%202006,%20PhD.pdf de Miranda. Structures Generated by Higher-Order Grammars and the Safety Constraint, 2006, PhD]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Ong/Rabin.%20Decidability%20of%20Second-Order%20Theories%20and%20Automata%20on%20Infinite%20Trees,%201969.pdf Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees, 1969]

==Трёхзначная абстракция и её приложения в Model Checking==
'''Орна Грумберг ([http://www.cs.technion.ac.il/~orna/ Orna Grumberg]), TECHNION — Технический университет Израиля'''

===Ссылки===
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Grumberg_Abs_09.pdf Аннотация автора]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Grumberg/Grumberg.%20Compositional%20Verification%20and%203-Valued%20Abstractions%20Join%20Forces.pdf Compositional Verification and 3-Valued Abstractions Join Forces]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Grumberg/Grumberg.%20A%20Game-Based%20Framework%20for%20CTL%20Counter-Examples%20and%203-Valued%20Abstraction-Refinement.ps.gz A Game-Based Framework for CTL Counter-Examples and 3-Valued Abstraction-Refinement]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Grumberg/Grumberg-abstraction-and-refinement.pdf Abstraction and Refinement in Model Checking]

==Механизированные семантики==
'''Ксавье Леруа ([http://pauillac.inria.fr/~xleroy/ Xavier Leroy]), INRIA, Франция'''

===Ссылки===
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Leroy_Abs_09.pdf Аннотация автора]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Leroy/slides.pdf Слайды к лекции]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Leroy/handout.pdf Раздаточный материал к лекции]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Leroy/Grall,%20Leroy.%20Coinductive%20big-step%20operational%20semantics.pdf Grall, Leroy. Coinductive big-step operational semantics]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Leroy/Nipkow.%20Winskel%20is%20(almost)%20Right_%20Towards%20a%20Mechanized%20Semantics%20Textbook.ps Nipkow. Winskel is (almost) Right_ Towards a Mechanized Semantics Textbook]
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Leroy/coq-hurry.pdf Bertot. Coq in a Hurry]

==Эффективный анализ стохастических процессов и игр с бесконечным числом состояний==
'''Антонин Кучера ([http://www.fi.muni.cz/usr/kucera/ Antonin Kučera]), Masaryk University, Чехия'''

===Ссылки===
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Kucera_Abs_09.pdf Аннотация автора]

==Синтаксический контроль утечек и освобождения информации==
'''Андрей Сабельфельд ([http://www.math.chalmers.se/~andrei/ Andrey Sabelfeld]), Gothenburg University, Швеция'''

===Ссылки===
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Sabelfeld_Abs_09.pdf Аннотация автора]

==Использование политик конфиденциальности (security policies) для написания безопасного (secure) ПО==
'''Эндрю Майерс ([http://www.cs.cornell.edu/andru/ Andrew Myers]), Cornell University, США'''

===Ссылки===
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Myers_Abs_09.pdf Аннотация автора]

==Два приложения систем доказательства теорем==
'''Тобиас Нипков ([http://www4.informatik.tu-muenchen.de/~nipkow/ Tobias Nipkow]), Технический университет Мюнхена, Германия'''

===Ссылки===
*[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/working_material/Abstracts/Nipkow_Abs_09.pdf Аннотация автора]

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

[http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0806000-Kupferman.MP3 Купферман], [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0806001-Jager-1.MP3 Ягер], [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0806002-Sabelfeld-discussion.MP3 Сабельфельд+обсуждение], [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0808000-Esparsa-2.MP3 Эспарза], [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0808001-Kucera-1.MP3 Кучера], [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0808002-Kupferman.MP3 Купферман], [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0808003-Ong-4-discussion.MP3 Онг+обсуждение], [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0814000-Nipkow-1-discussion.MP3 Нипков+обсуждение], [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0815000-Leroy.MP3 Леруа], [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0815001-Gordon.MP3 Гордон], [http://edu.mmcs.sfedu.ru/~ulysses/Edu/Marktoberdorf_2009/audio/V0815002-Grumberg.MP3 Грумберг].

==Примечания==
<references />

[[Категория:Летняя школа в г. Марктобердорф 2009]]