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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
(→‎Осень 2007 года)
(→‎Ссылки)
 
Строка 4: Строка 4:
  
 
[[Категория:Архив спецсеминаров кафедры математической кибернетики]]
 
[[Категория:Архив спецсеминаров кафедры математической кибернетики]]
 +
 +
== Весна 2010 года ==
 +
 +
{| class="wide" width="100%"
 +
! Дата
 +
! Тема доклада
 +
! Докладчик
 +
|-
 +
| 19 февраля
 +
| Организационное собрание
 +
|
 +
|-
 +
| 26 февраля
 +
| Проверка достижимости для модели программ с вызовами (по статье J.  Esparza "Building a Software Model Checker")
 +
| [[Студенты кафедры математической кибернетики|Подымов Владислав]]
 +
|-
 +
| 5 марта
 +
| Проверка достижимости для модели программ с вызовами (по статье J.  Esparza "Building a Software Model Checker") (продолжние)
 +
| [[Аспиранты кафедры математической кибернетики|Щербина Владислав]]
 +
|-
 +
| 19 марта
 +
| Алгоритмы преобразования регулярных выражений и автоматов в системе AMoRe
 +
| Алиса Ковтунова
 +
|-
 +
| 26 марта
 +
| Алгоритмы преобразования регулярных выражений и автоматов в системе AMoRe  (продолжение)
 +
| Алиса Ковтунова
 +
|-
 +
| 2 апреля
 +
| Алгоритмические метатеоремы для разрешимых задач верификации моделей бесконечных систем относительно спецификаций логики линейного времени
 +
| Игорь Коннов
 +
|}
 +
 +
== Весна 2009 года ==
 +
 +
{| class="wide" width="100%"
 +
! Дата
 +
! Тема доклада
 +
! Докладчик
 +
|-
 +
| 6 марта
 +
| Методы формальной верификации криптографических протоколов <ref> Косачёв Александр Сергеевич, Пономаренко Вера Николаевна. [http://ipv6.ispras.ru/Verification_of_security.pdf Анализ подходов к верификации функций безопасности и мобильности], ИСП РАН, 2004  </ref> <ref> Дмитрий Масюк. [http://mathcyb.ru/mediawiki/images/3/38/Dmasyuk.practice.v0.pdf Отчёт о производственной практике] </ref>
 +
| [[Студенты кафедры математической кибернетики|Масюк Дмитрий Викторович]]
 +
|-
 +
| 13 марта
 +
| Задачи и проблемы реорганизации программ
 +
| [[Студенты кафедры математической кибернетики|Татьяна Новикова]]
 +
|-
 +
| 20 марта
 +
| Об одном алгоритме поиска дублированных фрагментов кода <ref> Raghavan Komondoor, Susan Horwitz. [http://mathcyb.ru/mediawiki/images/1/1a/Pldi03-paper.pdf Eliminating Duplication in Source Code via Procedure Extraction], 2004 </ref> <ref> Raghavan Komondoor. [http://mathcyb.ru/mediawiki/images/6/69/Raghavan.thesis.pdf Automated duplicated-code detection and procedure extraction] , Ph.D. thesis, 2003</ref> <ref> Raghavan Komondoor, Susan Horwitz. [http://mathcyb.ru/mediawiki/images/f/f4/Sas01.pdf Using Slicing to Identify Duplication in Source Code], 2001</ref>
 +
| [[Студенты кафедры математической кибернетики|Татьяна Новикова]]
 +
|-
 +
| 27 марта
 +
| Генерация полиномиальных инвариантов цикла из присваиваний <ref> Laura Kovacs. [http://mtc.epfl.ch/~likovacs/pub/PhDKovacs.pdf 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. [http://mathcyb.ru/mediawiki/images/1/17/Concatenation_state_machines.pdf Concatenation State Machines and Simple Functions]</ref>
 +
| [[Студенты кафедры математической кибернетики|Александр Якушкин]]
 +
|-
 +
| 17 апреля
 +
| Equivalence of simple grammars <ref> Cdric Bastien, Jurek Czyzowicz, Wojciech Fraczak and Wojciech Rytter. [http://mathcyb.ru/mediawiki/images/d/dd/Equivalence_of_simple_grammars.pdf Prime Normal Form and Equivalence of Simple Grammars]</ref>
 +
| [[Студенты кафедры математической кибернетики|Александр Якушкин]]
 +
|}
 +
 +
== Осень 2008 года ==
 +
 +
{| class="wide" width="100%"
 +
! Дата
 +
! Тема доклада
 +
! Докладчик
 +
|-
 +
| 3 октября
 +
| Спецификация и верификация объектно-ориентированных программ, по материалам лекций Рустана Лейно <ref> [http://asimod.in.tum.de/2008/Leino_Abs_08.pdf] </ref> <ref> [http://asimod.in.tum.de/2008/Leino.pdf] </ref>
 +
| [http://lvk.cs.msu.su/~konnov Коннов Игорь]
 +
|-
 +
| 10 октября
 +
| Использование временных автоматов для задач верификации и синтеза программных систем <ref> Thomas A. Henzinger [http://www.eecs.berkeley.edu/~tah/Publications/the_theory_of_hybrid_automata.pdf The Theory Of Hybrid Automata] </ref> <ref> [http://www.uppaal.com UPPAAL model checker] </ref>
 +
| [http://lvk.cs.msu.su/~peterbul Булычёв Пётр Евгеньевич]
 +
|-
 +
| 24 октября
 +
| Равномерная проблема останова и синтез функций ранжирования
 +
| Влад Щербина
 +
|-
 +
| 31 Октября
 +
| Какая польза от многоленточных автоматов?
 +
| [[Захаров Владимир Анатольевич]]
 +
|-
 +
| 7 ноября
 +
| Техника следов в разрешении проблемы эквивалентности для алгебраических моделей программ
 +
| [[Подловченко Римма Ивановна]]
 +
|-
 +
| 14 ноября
 +
| Программы с зацеплениями состояний и простые функции
 +
| [[Студенты кафедры математической кибернетики|Александр Якушкин]]
 +
|}
 +
 +
== Весна 2008 года ==
 +
{| class="wide" width="100%"
 +
! Дата
 +
! Тема доклада
 +
! Докладчик
 +
|-
 +
| 22 февраля
 +
| О проблеме эквивалентности операторных программ
 +
| [[Захаров Владимир Анатольевич]]
 +
|-
 +
| 15 марта
 +
|  Minimization of lattice finite automata and its application to the decomposition of lattice languages <ref> Yongming Li, Witold Pedrycz, 2007, [http://portal.acm.org/citation.cfm?id=1243507.1243662  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, [http://www.cs.technion.ac.il/users/orna/submitted-ATVA05-multival.ps.gz Multi-Valued Model Checking Games]. </ref> <ref> Orna Kupferman Yoad Lustig, 2007, [http://www.cs.huji.ac.il/~ornak/publications/atva07.pdf  Latticed Simulation Relations and Games]</ref> <ref> Marsha Chechick, Benet Devereux, Arie Gurfinkel, Steve Easterbrook, 2004, [http://www.cs.toronto.edu/~chechik/pubs/tosem04.pdf Multi-Valued Symbolic Model-Checking] </ref>
 +
| [http://lvk.cs.msu.su/~peterbul Булычёв Пётр Евгеньевич]
 +
|-
 +
| 11 апреля
 +
| Применение техники следов для распознавания эквивалентности схем программ
 +
| [[Студенты кафедры математической кибернетики|Герасимов Сергей Алексеевич]]
 +
|-
 +
| 18 апреля
 +
| Коммутативная эквивалентность схем программ
 +
| [[Студенты кафедры математической кибернетики|Герасимов Сергей Алексеевич]]
 +
|-
 +
| 25 апреля
 +
| Применение алгоритмов анти-унификации к задаче поиска клонов в исходных кодах программ. Средство Clone Digger. <ref> Peter Bulychev, Marius Minea, 2008 [http://clonedigger.sourceforge.net/duplicate_code_detection_bulychev_minea.pdf Duplicate Code Detection Using Anti-Unification] </ref> <ref> [http://clonedigger.sourceforge.net Clone Digger: the tool for finding duplicate code in Python and Java] </ref>
 +
| [http://lvk.cs.msu.su/~peterbul Булычёв Пётр Евгеньевич]
 +
|}
 +
 +
== Осень 2007 года ==
 +
 +
{| class="wide" width="100%"
 +
! Дата
 +
! Тема доклада
 +
! Докладчик
 +
|-
 +
| 28 сентября
 +
| По материалам конференции WING 2007
 +
| [http://lvk.cs.msu.su/~konnov Коннов Игорь]
 +
|-
 +
| 5 октября
 +
| Элиминация кванторов в линейных арифметических теориях
 +
| [[Аспиранты кафедры математической кибернетики|Щербина Владислав]]
 +
|-
 +
| 12 октября
 +
| Изоморфизм Карри-Ховарда
 +
| [[Аспиранты кафедры математической кибернетики|Щербина Владислав]]
 +
|-
 +
| 19 октября
 +
| Минимальность и тупиковость многоленточных автоматов
 +
| Хачатрян Владимир Ервандович
 +
|-
 +
| 26 октября
 +
| Язык UML
 +
| [[Студенты кафедры математической кибернетики|Немцан М.Ю.]]
 +
|-
 +
| 2 ноября
 +
| Верификация UML
 +
| [[Студенты кафедры математической кибернетики|Немцан М.Ю.]]
 +
|-
 +
| 9 ноября
 +
| Верификация UML
 +
| [[Студенты кафедры математической кибернетики|Немцан М.Ю.]]
 +
|-
 +
| 16 ноября
 +
| Логические методы в информационной безопасности. BAN-логика. <ref>  Michael Burrows, Martín Abadi, Roger Needham, 1996, [http://citeseer.ist.psu.edu/burrows90logic.html A Logic of Authentication]. </ref> <ref> Colin Boyd, Wenbo Mao, 1993, [http://citeseer.ist.psu.edu/boyd93limitation.html On a Limitation of BAN Logic]. </ref>
 +
| [[Студенты кафедры математической кибернетики|Масюк Дмитрий Викторович]]
 +
|-
 +
| 23 ноября
 +
| Логические методы в информационной безопасности. BAN-логика. (продолжение)
 +
| [[Студенты кафедры математической кибернетики|Масюк Дмитрий Викторович]]
 +
|-
 +
| 30 ноября
 +
| Алгебраические модели продукционной логики и возможности их применения в интеллектуальных системах
 +
| Махортов Сергей Дмитриевич <br> Воронежский государственный университет
 +
|-
 +
| 7 декабря
 +
| Теория конформности для функционального тестирования программных систем на основе формальных моделей
 +
| Бурдонов Игорь Борисович <br> ИСП РАН
 +
|}

Текущая версия на 13:58, 30 января 2014

Ссылки

<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 декабря Теория конформности для функционального тестирования программных систем на основе формальных моделей Бурдонов Игорь Борисович
ИСП РАН
Источник — «https://mk.cs.msu.ru/index.php?title=Теоретические_проблемы_программирования_(Архив)&oldid=624»