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

Материал из Кафедра математической кибернетики
Перейти к: навигация, поиск
(Весна 2010 года)
(Весна 2009 года)
Строка 1: Строка 1:
== Весна 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 года ==
 
== Осень 2008 года ==
  

Версия 13:53, 30 января 2014

Осень 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 декабря Теория конформности для функционального тестирования программных систем на основе формальных моделей Бурдонов Игорь Борисович
ИСП РАН

Ссылки

<references/>