Computer Science семинар (весна 2012)

Общая информация
Семестрвесна 2012
Дата начала19.02.2012
Количество пар10
Язык курсарусский
Видеоhttp://www.lektorium.tv/course/?id=22868
Лекции Подсказка: слайды, видеозапись и другие материалы лекции доступны со страницы лекции, попасть на которую можно, нажав на её название.

1. Как не ошибиться с определением безопасности: о пользе authenticated encryption в теории и практике (Игорь Жирков, ИТМО/CS центр)
(19.02.2012 - 15:35 - 17:10)

Лекция посвящена тому, как определить понятие "безопасность" в различных ситуациях и в зависимости от возможностей злоумышленника. Будет проиллюстрировано, как небрежное отношение к формальным определениям приводит к уязвимостям в реальных системах (ASP.NET, CAPTCHA) на примере широко распространенного режима шифрования CBC. Конструктивным итогом будет простой метод, позволяющий защитить систему от активного злоумышленника.
2. Verifying Specifications with Proof Scores in CafeOBJ (Kokichi Futatsugi, Japan Advanced Institute of Science and Technology)
(31.03.2012 - 15:00 - 16:35)

Verifying specifications is still one of the most important undeveloped topics in software engineering. It is important because quite a few critical bugs are caused at the level of domains, requirements, and/or designs. It is also important for the cases where no program codes are generated and specifications are analyzed/verified only for justifying models of problems in real world.

In this talk, a survey of our research activities in verifying specifications is given. After explaining fundamental issues and importance of verifying specifications, the proof score approach in CafeOBJ and its applications to several areas are described.

http://www.lektorium.tv/lecture/?id=13698
3. Обнаружение текста на изображениях (Наталья Васильева, HP Labs)
(08.04.2012 - 13:00 - 14:35)

Лекция посвящена современным подходам и алгоритмам обнаружения текста на изображениях. Решение данной задачи является обязательным для последующего распознавания текста, а также имеет ряд других применений. Будут рассаматриваться различные классы изображений, такие как сканированные документы, фотографии, изображения графиков и диаграмм. Каждый из этих классов требует отдельного подхода: алгоритмы, хорошо работающие для одного из классов, могут быть не применимы для изображений другого класса. Точность существующих алгоритмов обнаружения текста в сканированных документах может превышать 99% , в то время как обнаружение текстовых блоков произвольного размера на фотографиях и графиках до сих пор остается актуальной областью исследований. http://www.lektorium.tv/lecture/?id=13721
4. Технологии формирования, обработки и визуализации стереоскопических "3D" изображений (Алексей Колесов, СПбГУТ)
(15.04.2012 - 13:00 - 15:35)

На лекции будет дан краткий обзор технологий получения, редактирования и воспроизведения стереоскопических "3D" изображений, а также уделено внимание алгоритмическим вопросам. http://www.lektorium.tv/lecture/?id=13739
5. Адаптация алгоритма решения задачи квадратичного программирования применительно к моделированию клепочного процесса деталей (Сергей Якунин, СПбГПУ и Computer Science центр)
(29.04.2012 - 13:00 - 14:35)

Контактная задача, возникающая при моделировании клепочного соединения деталей, после дискретизации методом конечных элементов и редукции переменных может быть сведена к задаче минимизации квадратичного функционала потенциальной энергии системы с линейными ограничениями в виде неравенств. Для ее решения наиболее эффективным считается алгоритм Гольдфарба-Иднани (Goldfarb-Idnani), который позволяет получить решение быстро и с высокой точностью. В математической библиотеке IMSL этот метод реализован с модификацией Пауэлла (Powell), которая повышает численную устойчивость метода для плохо обусловленных матриц. Алгоритм модифицирован с тем, чтобы максимально учесть особенности поставленной задачи:
  • матрица ограничений имеет простую структуру (один или два ненулевых числа в каждой строке);
  • вектор сил с результирующим набором активных ограничений (выполненных в виде равенств);
  • при решении некоторого набора задач решение предыдущей задачи служит начальным приближением для последующей задачи.
После внедрения указанных модификаций время работы алгоритма сократилось практически вдвое на тестовых задачах. http://www.lektorium.tv/lecture/?id=13764
6. Моделирование динамики в компьютерных играх, приложениях виртуальной реальности и тренажерах (Андрей Морозов, СимЭкс)
(13.05.2012 - 15:35 - 17:10)

  • Постепенное нарастание вычислительных мощностей компьютеров приводит к возможности создания предельно сложных и хорошо детализированных виртуальных миров, при этом все более приближая их к реальности. И реальность может достигаться не только за счет красоты отображения, но и с помощью качественной физической модели. О ней мы и поговорим.
  • Историческая справка. Этапы развития. Какие явления и сущности можно моделировать: тела/твердые тела; движение и взаимодействие тел; шарниры, связи и пружины; мягкие ткани и веревки; разрушаемые и деформируемые тела; жидкости и газы.
  • Что нам дает для этого современная наука: механика (кинематика, динамика); численные методы; вычислительная геометрия; программирование и структуры данных.
http://www.lektorium.tv/lecture/?id=13778
7. Faculty of informatics university of Lugano, Switzerland
(19.05.2012 - 18:15 - 19:00)

http://www.lektorium.tv/lecture/?id=13818
8. Computational Science – modeling approaches and algorithms (Igor Pivkin, University of Lugano, Switzerland)
(19.05.2012 - 19:15 - 20:05)

High performance computing can play a catalytic role in advancing physics, biology and medicine at all scales. Increasing power of supercomputers stimulate computational scientists to integrate numerous processes across many spatial and temporal scales in simulations. However, new scalable algorithms are required for simulations of multiscale phenomena encountered in physical and biological systems. In this talk, we will discuss some of the multiscale modeling approaches and related computational algorithms.
9. Service Oriented Computing with Resource Oriented Architectures (Cesare Pautasso, University of Lugano, Switzerland)
(19.05.2012 - 20:05 - 20:45)

Recent technology trends in service oriented computing indicate that a solution eliminating the perceived complexity of the WS-* standard technology stack may be in sight: advocates of representational state transfer (REST) have come to believe that their ideas explaining why the World Wide Web works are just as applicable to solving enterprise application integration problems and to radically simplifying the "plumbing" of service-oriented architectures. In this lecture, we introduce the area of service oriented computing and give an update on how the REST architectural style has been recently rediscovered to become the foundation for so-called "RESTful Web services." and "Resource Oriented Architectures". http://www.lektorium.tv/lecture/?id=13819
10. Local proof transformations for flexible interpolation and proof reduction (Prof. Natasha Sharygina, University of Lugano, Switzerland)
(20.05.2012 - 11:15 - 12:50)

Model checking based on Craig's interpolants ultimately relies on efficient engines, such as SMT-Solvers, to log proofs of unsatisfiability and to derive the desired interpolant by means of a set of algorithms known in literature. These algorithms, however, are designed for proofs that do not contain mixed predicates. In this talk I will present a technique for transforming the propositional proof produced by an SMT-Solver in such a way that mixed predicates are eliminated. There exists a number of cases in which mixed predicates arise as a consequence of state-of-the-art solving procedures (e.g., lemma on demand, theory combination, etc.). In such cases our technique can be applied to allow the reuse of known interpolation algorithms. I will then present a new approach to proof reduction, situated among the purely post-processing methods. The main idea is to reduce the proof size by eliminating redundancies of occurrences of pivots along the proof paths. This is achieved by matching and rewriting local contexts into simpler ones. In our approach, rewriting can be easily customized in the way local contexts are matched, in the amount of transformations to be performed, or in the different application of the rewriting rules. I will provide experimental evaluation of our technique on a set of SMT and SAT benchmarks, which shows considerable reduction in the proofs size. http://www.lektorium.tv/lecture/?id=13820
Ваша оценка: Пусто Средняя: 5 (1 голос)
Share |
Наталья Васильева
Наталья Васильева
Kokichi Futatsugi
Cesare Pautasso
Наталья Васильева
Igor Pivkin, Cesare Pautasso
Kokichi Futatsugi
Cesare Pautasso