Теоретические проблемы программирования
Спецсеминар проходит по пятницам с 16:20 до 17:55, ауд. 612.
Начало работы спецсеминара 22 сентября 2017 г.
Содержание
Тематика семинара
Математические модели программ и вычислений.
Формальные методы анализа и верификации программ.
Проблема эквивалентности и эквивалентных преобразований в моделях вычислений.
в 2014-15 учебном году семинар проводился совместно с научно-исследовательским семинаром Математическая криптография (рук. М.И. Анохин, Н.П. Варновский).
Руководители
2017-18 учебный год
| Дата | Тема доклада | Докладчик |
|---|---|---|
| 13 октября | Решение проблемы распознавания для программных схем с коммутативными и обратимыми функциями.
Доклад по статье Ashok K.Chandra "On the Decision Problems of Program Schemas with Commutative and Invertible Functions" В статье рассматриваются частично интерпретируемые унарные схемы, в которых некоторые функции указаны как коммутативные, а некоторые как обратимые. Показано, что если присутствуют либо коммутативные, либо обратимые функции, проблема разрешима, но как только появляются и коммутативные, и обратимые функции, проблема становится неразрешимой. Эти результаты также рассмотрены в приложении к конечным автоматам на многомерных бесконечных лентах. |
Е. Докшина
|
| 6 октября | Система правил для динамической верификации трасс событий.
Доклад по статье H. Barringer, A. Goldberg, K. Havelund, K. Sen "Rule-Based Runtime Verification" В статье описываются принципы работы программного средства, решающего следующую задачу. Имеется программа, работающая в режиме "чёрного ящика". В программе включен отладочный вывод: время от времени она предоставляет сообщения, содержащие информацию о значениях некоторых переменных. Требуется проверить, удовлетворяет ли текущая посланная последовательность сообщений заданным требованиям, в режиме он-лайн: выдавать результаты о выполнении требований по мере получения сообщений. Для решения этой задачи авторами предлагается особый логический формализм (Eagle): система правил, с одной стороны являющихся элементами синтаксиса формул, а с другой - описывающих способ перевычисления информации об истинности формул в режиме он-лайн. В предлагаемом формализме могут быть легко переформулированы требования, изначально записанные в ряде других известных логик, включая произвольные требования, выраженные формулами логики линейного прошлого времени (past-time LTL). Этот формализм и будет обсуждаться на семинаре. |
В.В. Подымов |
| 29 сентября | Верификация преобразований исходных кодов программ посредством проверки эквивалентности.
Доклад по статье K.C. Shashidhar, Maurice Bruynooghe, Francky Catthoor, Gerda Janssens "Verification of Source Code Transformations by Program Equivalence Checking" Как правило, когда алгоритмы для обработки цифровых сигналов адаптируются для работы в энергоэффективных и эффективно функционирующих встроенных системах, применяется комбинация ручных и автоматических преобразований. Это порождает сложную задачу верификации. Задача верификации упрощается при конвертирования кода в DSA-форму (dynamic single assignment form). Данная статья описывает метод доказательства эквивалентности двух программ в DSA-форме, в которых индексация элементов массивов и условия завершения циклов являются (кусочно заданными) аффинными выражениями. Для таких программ может быть использовано геометрическое моделирование и сразу для наборов элементов может быть показано, что результат вычислений обеих программ представляет собой одну и ту же функцию от входных данных. |
М.М. Аббас
|
| 22 сентября | Рещение задачи минимизации для одного вида детерминированных временных автоматов.
Доклад по статье Aleksandr Tvardovskii, Nina Yevtushenko "On minimization of Timed Finite State Machines" В этой статье показано, что для одной разновидности конечных временных автоматов с ограничениями на сроки обработки входного сигнала, задержкой выходного сигнала и тайм-аутом задача минимизации автоматов по числу состояний может быть сведена к аналогичной задаче для конечных детерминированных синхронных автоматов Мили. |
Е.М. Винарский |
2016-17 учебный год
| Дата | Тема доклада | Докладчик |
|---|---|---|
| 7 апреля | Проверка эквивалентности программ с неинтерпретируемыми функциями и целочисленной арифметикой.
Доклад по статье N.P. Lopes, J. Monteiro "Automatic equivalence checking of programs with uninterpreted functions and integer arithmetic" Доказательство эквивалентности программ имеет несколько важных приложений, в таких отраслях, как алгоритмы распознавания, регрессионное тестирование, тестирование сделанных компилятором оптимизаций и проверка утечек потоков информации. Несмотря на то что данная тема обладает важными приложениями, наука в проверки программ на эквивалентность не достигла серьёзных успехов за последние десятилетие в виду сложности этой задачи. В рассматриваемой статье предложен первая полуразрешающая процедура для автоматической проверки частичной эквивалентности двух программ, использующих неинтерпретируемые функции и работающих над целочисленной арифметикой (UF + IA). Предлагаемый алгоритм применим, в частности, к программам с вложенными циклами. Вначале проводится преобразование неинтерпретируемых функций (UF) в целочисленные полиномы, которые позволяют точно суммировать циклы с вхождениями UF, использующих рекурсию. Затем алгоритм проверки на эквивалентность переходит к свободным от циклов программам, оперирующих только целыми числами. |
Е.М. Винарский, В.В. Подымов |
| 31 марта | Распознавание вредоносных программ на основе их семантического анализа.
Доклад по статье M.Christodorescu et al. "Semantics-aware malware detection" Вирусы разрабатываются так чтобы существовать во множестве вариантов, чтобы их нельзя было обнаружить в коде зараженного файла по какой-то конкретной последовательности байт. В статье предлагается искать вирус по шаблонам моделирующим некоторое характерное для вирусов поведение. Показано что задача проверки совпадения такого шаблона в общем случае не разрешима. Предложен и программно реализован алгоритм успешно обнаруживающий некоторые семейства вирусов. |
М.Аббас, П.Булгаков |
| 24 марта | Механизация минимизации детерминированных обобщенных автоматов Бюхи.
Доклад по статье S. Baarir, A. Duret-Lutz “Mechanizing the Minimization of Deterministic Generalized Büchi Automata” Рассматриваются методы получения и минимизации детерминированных автоматов Бюхи для разных классов свойств. Метод минимизации сводится к задаче выполнимости булевых формул. Представляются тесты, которые реализуют все эти методы. |
З. Джусупекова
Г. Темербекова |
| 17 марта | Простые алгоритмы анализа сетей Петри.
Продолжение доклада по статье A. Finkel, J. Leroux "Recent and Simple Algorithms For Petri Nets" В статье рассказывается о сетях Петри, а также о проблемах достижимости, покрываемости и ограниченности для сетей Петри. Представлен новый, использующий инварианты, подход для разрешения этих проблем, который сравнительно проще алгоритмов, предложенных раннее. |
Е. Таратута
|
| 10 марта | Простые алгоритмы анализа сетей Петри.
Доклад по статье A. Finkel, J. Leroux "Recent and Simple Algorithms For Petri Nets" В статье рассказывается о сетях Петри, а также о проблемах достижимости, покрываемости и ограниченности для сетей Петри. Представлен новый, использующий инварианты, подход для разрешения этих проблем, который сравнительно проще алгоритмов, предложенных раннее. |
Е. Таратута
|
| 03 марта | Уравновешенные грамматики и их свойства.
Доклад по статье J. Berstel, L. Boasson "Balanced Grammars and their Languages" Balanced grammars are a generalization of parenthesis grammars in two directions. First, several kind of parentheses are allowed. Next, the set of right-hand sides of productions may be an infinite regular language. XML-grammars are a special kind of balanced grammars. It is shown that there exists a unique minimal balanced grammar equivalent to a given one. |
А. Гнатенко,
Е. Докшина
|
| 09 декабря | Задача обеспечения отказоустойчивости распределенных вычислительных систем.
Доклад по статье G.Klein, K.Elphinstone, G.Heiser et al. "seL4: Formal Verification of an OS Kernel" Статья про опыт разработки микроядра операционной системы от формальной спецификации будущей программы до реализации на C с доказательством корректности спецификации. |
П. Булгаков
|
| 02 декабря | Задача обеспечения отказоустойчивости распределенных вычислительных систем.
Продолжение доклада по статье "The Byzantine Generals Problem", L. Lamport, R. Shostak, M. Pease. ACM Transactions on Programming Languages and Systems. 1982, 4 (3), p. 382–401. На этот раз рассматриваем модель взаимодействующих процессов, в которой участники располагают средствами контроля целостности отправляемых сообщений. Насколько быстрее им удастся прийти к консенсусу? |
Н.С. Словеснов |
| 25 ноября | Проверка допустимости конфигураций модульных вычислительных систем реального времени.
|
А. Глонина (ЛВК ВМК МГУ) |
| 18 ноября | Задача обеспечения отказоустойчивости распределенных вычислительных систем.
Реферат статьи "The Byzantine Generals Problem", L. Lamport, R. Shostak, M. Pease. ACM Transactions on Programming Languages and Systems. 1982, 4 (3), p. 382–401. Reliable computer systems must handle malfunctioning components that give conflicting information to different parts of the system. This situation can be expressed abstractly in terms of a group of generals of the Byzantine army camped with their troops around an enemy city. Communicating only by messenger, the generals must agree upon a common battle plan. However, one or more of them may be traitors who will try to confuse the others. The problem is to find an algorithm to ensure that the loyal generals will reach agreement. It is shown that, using only oral messages, this problem is solvable if and only if more than two-thirds of the generals are loyal; so a single traitor can confound two loyal generals. With unforgeable written messages, the problem is solvable for any number of generals and possible traitors. Applications of the solutions to reliable computer systems are then discussed. |
Н.С. Словеснов |
| 11 ноября | Доказательство свойств функциональных программ методом насыщения равенствами.
Одним из декларируемых преимуществ функциональных языков программирования является простота преобразований, а также формулирования и доказательства свойств программ, что достигается главным образом за счет отсутствия побочных эффектов. Например, если мы знаем, что ∀x (f(x)=g(x)), то мы всегда можем заменить f(x) на g(x) (или их частные случаи) и наоборот в любом месте программы. Равенства такого вида имеют разные применения, такие, как верификация, преобразование программ и использование в качестве лемм для доказательства других подобных свойств. Во всех случаях желательно удостовериться в том, что равенство действительно выполняется. Доказательство таких эквивалентностей часто требуется проводить по индукции и коиндукции (для бесконечных структур данных). Насыщения равенствами (equality saturation) -- метод преобразования программ, заключающийся в применении преобразований к структуре данных, представляющей множество равенств над выражениями, и за счет этого способной хранить не одну программу, а целое множество семантически эквивалентных программ. Сам термин "насыщение равенствами" был введен в работе "Equality Saturation: A New Approach to Optimization" Тейта и др., где этот метод использовался для преобразования императивных программ. В насыщении равенствами каждое преобразование применяется недеструктивно и выводит новые равенства из уже существующих, расширяя таким образом множество представляемых программ. При этом потребление памяти значительно уменьшается за счет совмещения общих подвыражений. Насыщение равенствами можно применять для оптимизации -- при этом в конце из множества программ требуется выделить наилучшую. Насыщение равенствами можно также применять и для доказательства эквивалентности функций -- для этого определения функций преобразуются совместно до тех пор, пока не будет выведено равенство этих функций. В диссертационной работе рассматривается применение метода насыщения равенствами для индуктивного доказательства эквивалентности функций в нестрогом функциональном языке первого порядка. В отличие от императивных языков, в которых широко применяются циклы, в функциональных языках требуется работа с рекурсией более общего вида. Для индуктивного доказательства эквивалентности рекурсивных функций было введено преобразование, названное слиянием по бисимуляции, заключающегося в поиске двух подпрограмм, находящихся в отношении бисимуляции и удовлетворяющим синтаксическому признаку структурной рекурсии (защищенной в случае коиндукции). В работе доказано, что данный метод корректен для нетотального языка, в котором допустимо смешение конечных, бесконечных и частичных данных. Остальные правила преобразования были взяты из суперкомпиляции (а точнее из прогонки) и адаптированы для метода насыщения равенствами. |
С.А. Гречаник (ИПМ им.М.В.Келдыша РАН) |
| 21 октября | Продолжение доклада по статье P.A. Abdulla, B. Jonssen "Verifying Programs with Unreliable Channels": Information and Computation, v. 127, 1996, p. 91-101.. | Г.Г. Темербекова |
| 14 октября | Доклад по статье P.A. Abdulla, B. Jonssen "Verifying Programs with Unreliable Channels": Information and Computation, v. 127, 1996, p. 91-101..
Рассматриваются задачи верификация одного класса систем взаимодействующих процессов с конечным числом состояний, которые обмениваются данными с помощью неограниченных ненадежных FIFO каналов с возможностью потери сообщений. Показано, что для этого класса распределенных систем разрешимы некоторые задачи верификации, а именно проблемы достижимости, проблема безопасности относительно регулярных множеств трасс и проблемы живости относительно множеств состояний управления. При этом следует заметить (и это очень удивительно!), что 1) все перечисленные задачи алгоритмически неразрешимы в том случае, если для каналы абсолютно надежны и 2) сложность указанных задач неэлементарна. |
Г.Г. Темербекова |
| 7 октября | Обзор материалов 25-го Международного семинара "Concurrency, Specification and Programming (CS&P 2016)". | В.А. Захаров |
| 23 сентября | Памяти Риммы Ивановны Подловченко.
Рассказ о жизни и научных достижениях Риммы Ивановны Подловченко [1931-2016]. Римма Ивановна в 1953 г. окончила с отличием механико-математический факультет Московского Университета. В 1957-92 гг. она преподавала в Ереванском государственном университете, заведовала кафедрой вычислительной математики и кибернетики, кафедрой алгоритмических языков. В Московском университете работала с 1993 г. в должности ведущего научного сотрудника НИВЦ и в должности профессора на кафедре математической кибернетики факультета ВМиК. Научные интересы Риммы Ивановны охватывали широкий круг задач математической кибернетики и теории программирования, включая теорию моделей программ, теорию автоматов и теорию формальных языков. Р.И. Подловченко построила теорию алгебраических моделей программ, разработав ее методологию, понятийный аппарат и предложив целый ряд оригинальных методов анализа и преобразования программ. На основе этой теории она создала и применила новый понятийный и математический аппарат для построения систем эквивалентных преобразований в широких классах моделей вычислений В Московском университете она читала основные курсы лекций «Эквивалентные преобразования в моделях вычислений», «Избранные вопросы математической теории вычислений», а также специальные курсы лекций «Теория моделей программ», «Схемы программ и автоматы», «Математические основы функционального программирования». Она также руководила работой постоянного спецсеминара «Теоретические проблемы программирования». |
В.А. Захаров |
2014-15 учебный год
| Дата | Тема доклада | Докладчик |
|---|---|---|
| 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 ноября | Consistent network update without tagging
Designing of network update algorithms is urgent for development of SDN control software. A particular case of Network Update Problem is that of adding a set of forwarding rules into flow-tables of SDN switches (say, to install new paths in the network) or restoring seamlessly a given network configuration after some packet forwarding rules have been disabled (say, at the expiry of their time-outs). Some algorithms provide solutions to these problems but only with the help of tagging techniques. But is it possible to perform a consistent network update without tagging? We study this problem in the framework of a formal model of SDN, develop correct and safe network updating algorithms, and show that in some cases it is impossible to update consistently network configurations without resorting either to tagging or to priorities of packet forwarding rules. |
В.А. Захаров |
| 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) |
| 21 ноября | Быстрые алгоритмы проверки эквивалентности программ в моделях с полугрупповой семантикой.
В докладе будут представлены новые методы построения полиномиальных по времени алгоритмов проверки эквивалентности последовательных и рекурсивных программ в моделях программ с полугрупповой семантикой. |
В.В. Подымов |
| 28 ноября | Candidate One-Way Functions Based on Expander Graphs.
We suggest a candidate one-way function using combinatorial constructs such as expander graphs. These graphs are used to determine a sequence of small overlapping subsets of input bits, to which a hard-wired random predicate is applied. Thus, the function is extremely easy to evaluate: all that is needed is to take multiple projections of the input bits, and to use these as entries to a look-up table. It is feasible for the adversary to scan the look-up table, but we believe it would be infeasible to find an input that fits a given sequence of values obtained for these overlapping projections. The conjectured difficulty of inverting the suggested function does not seem to follow from any well-known assumption. Instead, we propose the study of the complexity of inverting this function as an interesting open problem, with the hope that further research will provide evidence to our belief that the inversion task is intractable. |
Л. Р. Ахметзянова |
| 05 декабря | Формальные модели и верификация свойств программ с использованием предметно-ориентированных языков.
В рамках работы, результаты которой представлены в докладе, предлагается подход к верификации сложных, наукоемких программных комплексов. Его суть в том, чтобы описывать их покомпонентно с помощью языков, адекватно отражающих специфику предметной области (предметно-ориентированных языков), которые при этом имеют заданную формальную семантику. Для построения таких языков и их формальной семантики разработано промежуточное представление на основе λ-исчисления с зависимыми типами. Результаты тестовых испытаний демонстрируют программную реализуемость предлагаемого подхода и возможности его применения для описания фрагментов реально существующего и используемого на практике программного комплекса. |
М.А. Кривчиков |
| 12 декабря | Possibilities and Limits of Fully Homomorphic Encryption.
What is a homomorphic encryption? What is it good for? Is it sufficient to make cloud computing secure? These questions are the most accute topics in modern cryptography, and they will be discussed in this talk. |
I. Bongartz |
| 19 декабря | Ontology-based Data Access: Theory and Practice.
Ontology-based data access (OBDA) is regarded as a key ingredient for the new generation of information systems. In the OBDA paradigm, an ontology defines a high-level global schema of (already existing) data sources and provides a vocabulary for user queries. An OBDA system rewrites such queries and ontologies into the vocabulary of the data sources and then delegates the actual query evaluation to a suitable query answering system such as a relational database management system or a datalog engine. This lecture will mainly focus on OBDA with the ontology language OWL 2 QL, one of three profiles of the W3C standard Web Ontology Language OWL 2, and relational databases, although other possible languages will also be discussed. It will cover the following topics:
- different architectures of OBDA systems; - practical OBDA with open source system Ontop (http://ontop.inf.unibz.it) |
M. Zakharyaschev (Birkbeck, University of London) |
| 27 февраля | О проблеме сведения доказательства стойкости протокола к проверке эквивалентности конечных автоматов.
Один из способов доказательства стойкости криптографических протоколов использует переход к символьной модели и проверку эквивалентности двух конечных автоматов, соответствующих реальной и идеальной моделям выполнения протокола. В докладе будет изложен способ неявного описания автоматов, которые могут быть использованы в этом качестве. Исследуется следующая проблема: имея такие описания для двух различных автоматов (соответствующих двум различным моделям работы сети) доказать, что они эквивалентны. |
А.А. Татузов (ИПИБ МГУ) |
| 22 апреля | Автоматизация проектирования электронных устройств Аннотация доклада. | Семинар компании Cadence design systems. |
Ссылки
<references/>
