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

Материал из Вики ИТ мехмата ЮФУ
Перейти к: навигация, поиск
(Новая страница: «Ниже приведён список курсов лекций, прочитанных в летней школе по верификации и формальны…»)
 
(→‎Анализ и верификация программ с помощью абстрактной интерпретации)
Строка 6: Строка 6:
 
В исследованиях по верификации программ самой популярной моделью для программы является ''система переходов'': тройка из множества состояний, его подмножества начальных состояний и бинарного отношения перехода на множестве состояний, которое является отношением порядка. Можно рассмотреть иерархию семантик программ, абстрагированных таким образом. Например, множество [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://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.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]].
  
 
===Ссылки===
 
===Ссылки===

Версия 20:33, 23 августа 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].

Ссылки

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