Теоретические проблемы программирования
Спецсеминар проходит по пятницам с 16:20 до 17:55, ауд. 508.
Начало работы спецсеминара 3 октября 2014 г.
Тематика семинара
Математические модели программ и вычислений.
Формальные методы анализа и верификации программ.
Проблема эквивалентности и эквивалентных преобразований в моделях вычислений.
Семинар проводится совместно с научно-исследовательским семинаром Математическая криптография (рук. М.И. Анохин, Н.П. Варновский).
Руководители
Расписание докладов
| Дата | Тема доклада | Докладчик |
|---|---|---|
| 19 сентября | Формальные грамматики после Карибского кризиса.
Формальные грамматики появились в конце 50-х гг. XX века, когда развитие вычислительной техники потребовало строго определить синтаксис языков программирования, а также подало надежду на машинную обработку естественных языков. К октябрю 1962 г. были в первом приближении разработаны основные понятия новой теории и получены некоторые результаты: системы перезаписи строк и иерархия Хомского, форма Бэкуса-Наура, синтаксический разбор с помощью рекурсивного спуска, лемма накачки и несколько неразрешимых задач. Эти ранние исследования определили первоначальное представление о формальных грамматиках, которое продолжает воспроизводиться и в современных учебниках по информатике. Исследования в области грамматик продолжались, однако, и после Карибского кризиса, и за прошедшие полвека представление о том, что такое формальная грамматика, несколько изменилось. Ошибочные понятия (такие как контекстно-зависимые грамматики Хомского и многочисленные производные модели) постепенно сошли на нет, и с их уходом устарели и породившие их принципы классификации. Новые виды грамматик принесли с собой представление о формальных грамматиках как о специализированной логике для описания синтаксиса; важную роль в этом сыграла работа Раундса (1988), описавшего различные виды грамматик как фрагменты логики первого порядка над позициями в строке. Цель данного доклада --- рассказать, как изменилось понятие о формальных грамматиках за полвека, какие виды грамматик известны сегодня, как они соотносятся друг с другом, и что с ними можно попытаться делать дальше. |
А.С. Охотин |
| 03 октября | Computational privacy in public clouds. Beyond the impossibility result.
It is widely believed that Fully Homomorphic Encryption (FHE) only is sufficient to provide the security of cloud computations. However, Marten van Dijk and Ari Juels in a recent paper showed that in some cases cryptography alone can’t enforce the privacy demanded by common cloud computing services, even with such powerful tools as FHE. Can we bypass this impossibility result? What extra requirements should be imposed a model of cloud computations to guarantee the privacy? These and other questions concerning the security issues of cloud computing will be discussed. |
Н.П. Варновский |
| 10 октября | Конечные автоматы в теории алгебраических моделей программ (методологический обзор).
Изучается преемственность методов распознавания эквивалентности для конечных автоматов и схем программ в алгебраических моделях программ. |
Р.И. Подловченко |
| 17 октября | On the composition of zero-knowledge proof systems.
We present some results by Goldreich and Krawczyk from the work with the same title (Proc. of ICALP'90 and SIAM J. on Computing, 1996, v.25, no. 1). By these results, zero-knowledge is not preserved under composition of protocols. |
М.И. Анохин |
| 24 октября | Syntactical characterization of LOGSPACE.
We study programs with the fixed set of variables and relationships between the complexity class containing all languages recognizable by such programs, and the complexity classes DLOGSPACE and NLOGSPACE. |
Д.А. Носов |
| 31 октября | Finite state transducers over semigroups.
Transducers over semigroups extend the concept of string transducers and may be used as a formal model of sequential reactive programs. We introduce a uniform techniques for building efficient procedures for checking functionality, $k$-valuedness, equivalence and inclusion for finite state transducers over semigroups. The obtained procedures are capable to decide equivalence for deterministic transducers in polynomial time, and check $k$-valuedness and decide equivalence in single exponential time for bounded valued transducers over semigroups that can be embedded into decidable groups. |
В.А. Захаров |
| 07 ноября | В.А. Захаров | |
| 12 ноября (ауд. 523) | On the verification of threshold-based fault-tolerant distributed algorithms.
Counter abstraction is a powerful tool for parameterized model checking, if the number of local states of the concurrent processes is relatively small. In recent work, we introduced parametric interval counter abstraction that allowed us to verify the safety and liveness of threshold-based fault-tolerant distributed algorithms (FTDA). Due to state space explosion, applying this technique to distributed algorithms with hundreds of local states is challenging for state-of-the-art model checkers. In this talk, we demonstrate that reachability properties of FTDAs can be verified by bounded model checking. To ensure completeness, we need an upper bound on the diameter, i.e., on the longest distance between states. We show that the diameters of accelerated counter systems of FTDAs, and of their counter abstractions, have a quadratic upper bound in the number of local transitions. Our experiments show that the resulting bounds are sufficiently small to use bounded model checking for parameterized verification of reachability properties of several FTDAs, some of which have not been automatically verified before. This part is based on the paper presented at CONCUR'14. Further, we demonstrate how the proof ideas from CONCUR'14 can be re-used to implement a bounded model checker for accelerated counter systems without applying counter abstraction. The model checker constructs a finite (and typically small) set of representative accelerated schedules that together visit all reachable configurations. Finally, each representative schedule is checked for feasibility within an SMT solver. Our preliminary experiments show that this new technique over-performs counter abstraction on our case studies by three orders of magnitude. |
Josef Widder, Igor Konnov (TU Vienna) |
Ссылки
<references/>
