Project Seminar 2019 2020 — различия между версиями

Материал из Wiki - Факультет компьютерных наук
Перейти к: навигация, поиск
Строка 21: Строка 21:
  
 
====Семинар 4 (3 октября).  ====
 
====Семинар 4 (3 октября).  ====
 +
Доклад Антона Гнатенко
 +
 +
====Семинар 5 (10 октября).  ====
 +
Доклад Антона Гнатенко.
 +
Анонс:
 +
Чернышова Дина Александровна
 +
 +
вт, 1 окт., 21:09
 +
 +
кому: Nikolay, Mikhail, Vladimir, Alexander, Alexander, Vladimir, я, Козачинский, Gleb, Евстропов, Alexey, Timur, Кутенин, Павел, Алексей, Катя, Ярослав, storozhenkoaa@yandex.ru, Michael, sergey, andrii.riazanov@gmail.com, brbauwens@gmail.com, tehadawest@gmail.com, vbezhentsev@gmail.com, eterniusgrv@gmail.com, s-luba@mail.ru, g.kabatyansky@skoltech.ru, egorovahelene@gmail.com, pguillon@math.cnrs.fr, a.chistopolskaia@gmail.com, Кузнецов, iablinnikov@edu.hse.ru, nsdobrokhotovamaykova@edu.hse.ru, korolenkov@inbox.ru, zhuk.dmitriy@gmail.com, argnatenko@edu.hse.ru, Подольский
 +
Добрый вечер!
 +
 +
Обращаю ваше внимание, что на следующей неделе семинар пройдет в четверг, 10 октября и в другой аудитории, R207!
 +
 +
10 октября на семинаре лаборатории теоретической информатики состоится доклад Антона Гнатенко "Спецификация
 +
и верификация конечных автоматов-преобразователей".
 +
 +
Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания
 +
поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Для формальной спецификации и верификации реагирующих систем такого рода требуются более
 +
сложные и выразительные средства спецификации, нежели традиционные темпоральные логики. В докладе будет предложена расширенная темпоральная логика Reg-CTL*, в которой темпоральные операторы параметризованы регулярными выражениями. Мы рассмотрим алгоритмы верификации
 +
автоматов-преобразователей относительно формул некоторых фраментов этой логики, а также её выразительные возможности. На правах "work in progress" будет изложена идея алгоритма верифкации относительно произвольных формул Reg-CTL*.
 +
 +
 +
 +
 +
====Семинар 6 (17 октября).  ====
 
Доклад Антона Гнатенко
 
Доклад Антона Гнатенко
  

Версия 14:45, 17 октября 2019

Расписание

Семинар проходить по четвергам с 18.10 по 19.30

Проведённые семинары

Семинар 1 (12 сентября).

Задача равенства нулю многочлена. Лемма Шварца-Зиппеля.


Семинар 2 (19 сентября).

Применение задачи равенства нулю многочлена для решения задачи о паросочетаниях. Дерандомизация задачи о равенстве нулю многочлена для случая небольшого числа ненулевых мономов.

Семинар 3 (26 сентября).

Дерандомизация задачи о равенстве нулю многочлена с помощью теорем типа Сильвестра-Галлаи.

Семинар 4 (3 октября).

Доклад Антона Гнатенко

Семинар 5 (10 октября).

Доклад Антона Гнатенко. Анонс: Чернышова Дина Александровна

вт, 1 окт., 21:09

кому: Nikolay, Mikhail, Vladimir, Alexander, Alexander, Vladimir, я, Козачинский, Gleb, Евстропов, Alexey, Timur, Кутенин, Павел, Алексей, Катя, Ярослав, storozhenkoaa@yandex.ru, Michael, sergey, andrii.riazanov@gmail.com, brbauwens@gmail.com, tehadawest@gmail.com, vbezhentsev@gmail.com, eterniusgrv@gmail.com, s-luba@mail.ru, g.kabatyansky@skoltech.ru, egorovahelene@gmail.com, pguillon@math.cnrs.fr, a.chistopolskaia@gmail.com, Кузнецов, iablinnikov@edu.hse.ru, nsdobrokhotovamaykova@edu.hse.ru, korolenkov@inbox.ru, zhuk.dmitriy@gmail.com, argnatenko@edu.hse.ru, Подольский Добрый вечер!

Обращаю ваше внимание, что на следующей неделе семинар пройдет в четверг, 10 октября и в другой аудитории, R207!

10 октября на семинаре лаборатории теоретической информатики состоится доклад Антона Гнатенко "Спецификация

и верификация конечных автоматов-преобразователей".

Конечные автоматы, задающие преобразования потоков входных сигналов в последовательности элементарных действий, являются простейшей моделью вычислений, пригодной для описания

поведения реагирующих систем. Это поведение проявляется в соответствии между потоком входных сигналов и последовательностью элементарных действий, выполняемых системой. Для формальной спецификации и верификации реагирующих систем такого рода требуются более
сложные и выразительные средства спецификации, нежели традиционные темпоральные логики. В докладе будет предложена расширенная темпоральная логика Reg-CTL*, в которой темпоральные операторы параметризованы регулярными выражениями. Мы рассмотрим алгоритмы верификации
автоматов-преобразователей относительно формул некоторых фраментов этой логики, а также её выразительные возможности. На правах "work in progress" будет изложена идея алгоритма верифкации относительно произвольных формул Reg-CTL*.



Семинар 6 (17 октября).

Доклад Антона Гнатенко

Предлагаемые статьи для рассказа на семинаре

1) Nitin Saxena, Progress on Polynomial Identity Testing https://eccc.weizmann.ac.il/report/2009/101/

2) Лекции Стэндфордского университета о PIT и совершенных паросочетаниях. https://cs.stanford.edu/~mpkim/notes/lec5.pdf

Преподаватели

Милованов Алексей, almas239@gmail.com