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

Формальные грамматики появились в конце 50-х гг. XX века, когда развитие вычислительной техники потребовало строго определить синтаксис языков программирования, а также подало надежду на машинную обработку естественных языков. К октябрю 1962 г. были в первом приближении разработаны основные понятия новой теории и получены некоторые результаты: системы перезаписи строк и иерархия Хомского, форма Бэкуса-Наура, синтаксический разбор с помощью рекурсивного спуска, лемма накачки и несколько неразрешимых задач. Эти ранние исследования определили первоначальное представление о формальных грамматиках, которое продолжает воспроизводиться и в современных учебниках по информатике.

Исследования в области грамматик продолжались, однако, и после Карибского кризиса, и за прошедшие полвека представление о том, что такое формальная грамматика, несколько изменилось. Ошибочные понятия (такие как контекстно-зависимые грамматики Хомского и многочисленные производные модели) постепенно сошли на нет, и с их уходом устарели и породившие их принципы классификации. Новые виды грамматик принесли с собой представление о формальных грамматиках как о специализированной логике для описания синтаксиса; важную роль в этом сыграла работа Раундса (1988), описавшего различные виды грамматик как фрагменты логики первого порядка над позициями в строке. Цель данного доклада --- рассказать, как изменилось понятие о формальных грамматиках за полвека, какие виды грамматик известны сегодня, как они соотносятся друг с другом, и что с ними можно попытаться делать дальше.

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.

Изучается преемственность методов распознавания эквивалентности для конечных автоматов и схем программ в алгебраических моделях программ.

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.

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.

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.

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.