Теоретические проблемы программирования (Архив)

Ссылки

<references/>

Весна 2010 года

Дата	Тема доклада	Докладчик
19 февраля	Организационное собрание
26 февраля	Проверка достижимости для модели программ с вызовами (по статье J. Esparza "Building a Software Model Checker")	Подымов Владислав
5 марта	Проверка достижимости для модели программ с вызовами (по статье J. Esparza "Building a Software Model Checker") (продолжние)	Щербина Владислав
19 марта	Алгоритмы преобразования регулярных выражений и автоматов в системе AMoRe	Алиса Ковтунова
26 марта	Алгоритмы преобразования регулярных выражений и автоматов в системе AMoRe (продолжение)	Алиса Ковтунова
2 апреля	Алгоритмические метатеоремы для разрешимых задач верификации моделей бесконечных систем относительно спецификаций логики линейного времени	Игорь Коннов

Весна 2009 года

Дата	Тема доклада	Докладчик
6 марта	Методы формальной верификации криптографических протоколов <ref> Косачёв Александр Сергеевич, Пономаренко Вера Николаевна. Анализ подходов к верификации функций безопасности и мобильности, ИСП РАН, 2004 </ref> <ref> Дмитрий Масюк. Отчёт о производственной практике </ref>	Масюк Дмитрий Викторович
13 марта	Задачи и проблемы реорганизации программ	Татьяна Новикова
20 марта	Об одном алгоритме поиска дублированных фрагментов кода <ref> Raghavan Komondoor, Susan Horwitz. Eliminating Duplication in Source Code via Procedure Extraction, 2004 </ref> <ref> Raghavan Komondoor. Automated duplicated-code detection and procedure extraction , Ph.D. thesis, 2003</ref> <ref> Raghavan Komondoor, Susan Horwitz. Using Slicing to Identify Duplication in Source Code, 2001</ref>	Татьяна Новикова
27 марта	Генерация полиномиальных инвариантов цикла из присваиваний <ref> Laura Kovacs. Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema , Ph.D. thesis, 2007 </ref>	Подымов Владислав Васильевич
3 апреля	Генерация полиномиальных инвариантов цикла из присваиваний (продолжение)	Подымов Владислав Васильевич
10 апреля	Concatenation state machines <ref> Wojciech Debski and Wojciech Fraczak. Concatenation State Machines and Simple Functions</ref>	Александр Якушкин
17 апреля	Equivalence of simple grammars <ref> Cdric Bastien, Jurek Czyzowicz, Wojciech Fraczak and Wojciech Rytter. Prime Normal Form and Equivalence of Simple Grammars</ref>	Александр Якушкин

Осень 2008 года

Дата	Тема доклада	Докладчик
3 октября	Спецификация и верификация объектно-ориентированных программ, по материалам лекций Рустана Лейно <ref> [1] </ref> <ref> [2] </ref>	Коннов Игорь
10 октября	Использование временных автоматов для задач верификации и синтеза программных систем <ref> Thomas A. Henzinger The Theory Of Hybrid Automata </ref> <ref> UPPAAL model checker </ref>	Булычёв Пётр Евгеньевич
24 октября	Равномерная проблема останова и синтез функций ранжирования	Влад Щербина
31 Октября	Какая польза от многоленточных автоматов?	Захаров Владимир Анатольевич
7 ноября	Техника следов в разрешении проблемы эквивалентности для алгебраических моделей программ	Подловченко Римма Ивановна
14 ноября	Программы с зацеплениями состояний и простые функции	Александр Якушкин

Весна 2008 года

Дата	Тема доклада	Докладчик
22 февраля	О проблеме эквивалентности операторных программ	Захаров Владимир Анатольевич
15 марта	Minimization of lattice finite automata and its application to the decomposition of lattice languages <ref> Yongming Li, Witold Pedrycz, 2007, Minimization of lattice finite automata and its application to the decomposition of lattice languages. </ref>	Кувалдин Кирилл Сергеевич
28 марта	Алгоритмы сжатия строковых данных
4 апреля	Проверка моделей на решётках (lattice model checking) <ref> Sharon Shoham, Orna Grumberg, 2005, Multi-Valued Model Checking Games. </ref> <ref> Orna Kupferman Yoad Lustig, 2007, Latticed Simulation Relations and Games</ref> <ref> Marsha Chechick, Benet Devereux, Arie Gurfinkel, Steve Easterbrook, 2004, Multi-Valued Symbolic Model-Checking </ref>	Булычёв Пётр Евгеньевич
11 апреля	Применение техники следов для распознавания эквивалентности схем программ	Герасимов Сергей Алексеевич
18 апреля	Коммутативная эквивалентность схем программ	Герасимов Сергей Алексеевич
25 апреля	Применение алгоритмов анти-унификации к задаче поиска клонов в исходных кодах программ. Средство Clone Digger. <ref> Peter Bulychev, Marius Minea, 2008 Duplicate Code Detection Using Anti-Unification </ref> <ref> Clone Digger: the tool for finding duplicate code in Python and Java </ref>	Булычёв Пётр Евгеньевич

Осень 2007 года

Дата	Тема доклада	Докладчик
28 сентября	По материалам конференции WING 2007	Коннов Игорь
5 октября	Элиминация кванторов в линейных арифметических теориях	Щербина Владислав
12 октября	Изоморфизм Карри-Ховарда	Щербина Владислав
19 октября	Минимальность и тупиковость многоленточных автоматов	Хачатрян Владимир Ервандович
26 октября	Язык UML	Немцан М.Ю.
2 ноября	Верификация UML	Немцан М.Ю.
9 ноября	Верификация UML	Немцан М.Ю.
16 ноября	Логические методы в информационной безопасности. BAN-логика. <ref> Michael Burrows, Martín Abadi, Roger Needham, 1996, A Logic of Authentication. </ref> <ref> Colin Boyd, Wenbo Mao, 1993, On a Limitation of BAN Logic. </ref>	Масюк Дмитрий Викторович
23 ноября	Логические методы в информационной безопасности. BAN-логика. (продолжение)	Масюк Дмитрий Викторович
30 ноября	Алгебраические модели продукционной логики и возможности их применения в интеллектуальных системах	Махортов Сергей Дмитриевич Воронежский государственный университет
7 декабря	Теория конформности для функционального тестирования программных систем на основе формальных моделей	Бурдонов Игорь Борисович ИСП РАН