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

== Ссылки ==

<references/>

[[Категория:Архив спецсеминаров кафедры математической кибернетики]]

== Весна 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> ИСП РАН
|}