Теория и практика функциональных и логических парадигм программирования и их реализация в высокопроизводительных вычислительных средах Исследовательский центр мультипроцессорных систем, ИПС РАН.

Публикации. Подготовлено к публикации: –Р.Ф. Гурин и С.А. Романенко, Язык программирования РЕФАЛ плюс. Монография, издание второе переработанное, (172 страницы). –A. Lisitsa, A.P. Nemytykh, Induction principles in verification via supercompilation. Submitted to ACM SIGPLAN 2007 Workshop on Partial Evaluation and Program Manipulation PEPM Принято к публикации: –S.M. Abramov, R. Glueck, Yu.A. Klimov, An universal resolving algorithm for inverse computation in a lazy language, In Proc. of the conference PSI-2006, Lecture Notes in Computer Science. –А.П. Лисица и А.П. Немытых, Верификация как параметрическое тестирование. (Эксперименты с суперкомпилятором SCP4.), Журнал Программирование. Опубликовано: –А.П. Лисица и А.П. Немытых, Работа над ошибками. В трудах конференции Программные системы: теория и приложения, Физматлит, Москва, том 1, стр: (37 страниц), –S. D. Mechveliani, A predicate calculas prover based on completion and boolean term algebra. Технический отчёт института RICAM, г. Линц, Австрия, 2006.

Поддержка и развитие реализации языка REFAL+. Запланировано: –Реализация системы программирования РЕФАЛ+ в среде языка программирования Java. Сделано: –Реализована стартовая версия run-time поддержки языка РЕФАЛ+ в среде языка программирования Java. –Разработана новая версия синтаксиса языка РЕФАЛ+. –Разработаны и частично реализованы механизмы меж- языкового взаимодействия из среды РЕФАЛ+. –Поддерживалась реализация языка РЕФАЛ+ под операционными системами Linux и Windows.

Поддержка реализации языка REFAL-5. Запланировано: –Оптимизация копирования данных средствами специализации. –Реализация элементов метавычислений равномерных по параметрам в интерпретаторе РЕФАЛ-5. Сделано: –В оптимизирующем компиляторе CREFAL разработана и реализована стартовая версия алгоритма специализации программ, позволяющего сократить копирование данных (т.е. максимальное использование данных, построенных программой, на последующих этапах её работы). –Реализованы алгоритмы (тестовая версия) вычислений равномерных по входным данным в интерпретаторе РЕФАЛа-5. –Поддерживалась реализация языка РЕФАЛ-5

Поддержка и развитие суперкомпилятора SCP4. Запланировано: –Изучение возможностей суперкомпилятора SCP4 для автоматического решения задач верификации программ. Сделано: –Изучались методы автоматизации математической индукции с целью верификации программ посредством суперкомпиляции. Полученные результаты исследований частично оформлены в виде научных статей. –Поддерживалась реализация суперкомпилятора SCP4. ( )

Поддержка и развитие системы автоматического поиска доказательств Думатель. Запланировано: –Разработка алгоритмов поиска логического вывода- верификации, использующих разбор случаев для конечно- значной области. –Разработка средств отслеживания хода поиска вывода свойств программ и разработка средств вмешательства в ход поиска. Сделано: –Развит и реализован алгоритм поиска логического вывода верификации, использующий метод пополнения в соединении с разбором случаев для конечно-значной области. –Разработаны и реализованы способ отслеживания хода поиска вывода и язык заданий подсказок пользователя. Метод разработан на основе представления поиска в виде последовательности деревьев состояния поиска вывода. ( )

Разработка методов верификации вычислительных систем. Запланировано: –Разработка подхода к процессу верификации как к равномерному (параметризованному) тестированию. Сделано: –Показана возможность использования нашего метода для верификации параметризованных (т.е. число процессоров в системе конечно, но неизвестно сколько) cache coherence протоколов с условиями глобальной корректности. –Автоматические доказательства корректности следующих cache coherence протоколов: Xerox PARC Dragon, IEEE Futurebus+, MOESI, MESI, MSI, The University of Illinois, DEC Firefly, Berkeley. –Успешные эксперименты по верификации модельных протоколов опи- санных в формализме сетей Петри: по постусловию и progress property. –На примере неудачной спецификации протокола Xerox PARC Dragon, дан- ной Ж. Дельзанно, показана возможность использования суперкомпилято- ра SCP4 для обнаружения ошибок спецификации и построения тестов на эти ошибки. –Построена формальная модель описывающая инструменты суперкомпи- ляции, использование которых достаточно для верификации рассматри- ваемого нами класса cache coherence протоколов. Доказана корректность этой формальной модели.

Международное сотрудничество. University of Copenhagen (Denmark) The University of Liverpool (United Kingdom) Johann Radon Institute for Computational and Applied Mathematics (RICAM) (Austrian Academy of Sciences)

Публикации. Подготовлено к публикации: –Р.Ф. Гурин и С.А. Романенко, Язык программирования РЕФАЛ плюс. Монография, издание второе переработанное, (172 страницы). –A. Lisitsa, A.P. Nemytykh, Induction principles in verification via supercompilation. Submitted to ACM SIGPLAN 2007 Workshop on Partial Evaluation and Program Manipulation PEPM Принято к публикации: –S.M. Abramov, R. Glueck, Yu.A. Klimov, An universal resolving algorithm for inverse computation in a lazy language, In Proc. of the conference PSI-2006, Lecture Notes in Computer Science. –А.П. Лисица и А.П. Немытых, Верификация как параметрическое тестирование. (Эксперименты с суперкомпилятором SCP4.), Журнал Программирование. Опубликовано: –А.П. Лисица и А.П. Немытых, Работа над ошибками. В трудах конференции Программные системы: теория и приложения, Физматлит, Москва, том 1, стр: (37 страниц), –S. D. Mechveliani, A predicate calculas prover based on completion and boolean term algebra. Технический отчёт института RICAM, г. Линц, Австрия, 2006.