Персональные инструменты
Вы здесь: Главная seminar

Семинар кафедры системного программирования

 

 

 

 

 

Ближайшее заседание: понедельник 13 ноября 2017 17-00 каб. А.Н. Терехова

Амелин Константин Сергеевич
Гражданские БПЛА: современные технологии и направления, проблемы и их возможные решения

В связи с увеличением роста применения сверхлегких БПЛА при решении задач гражданского применения, к таким аппаратам возрастают требования в техническом плане, к применяемому программному и математическому обеспечению, к системам безопасности, а также растет необходимость в унификации БПЛА и увеличения их потенциала. На семинаре будут представлены актуальные задачи при разработке сверхлегких БПЛА для гражданского применения, методы их решения, проблемы реализации таких решений, а также актуальные текущие проблемы при решении новых задач. Такие проблемы возникают при создании новых систем автопилотирования БПЛА, обработки данных, оптимизации полета БПЛА, при работе с дополнительными исполнительными механизмами. Будут представлены новые актуальные направления развития гражданских БПЛА, проблемы безопасности, а также задачи применения лазерных технологий при работе как обособленных БПЛА, так и их групп.


Прошедшие заседания 2017/2018 учебного года:

13 октября 2017
(пятница 17-00 каб. А.Н. Терехова)

Мордвинов Дмитрий Александрович
О неограниченной верификации, решателях дизъюнктов Хорна и символьном исполнении

За последние 3 года появилось несколько верификаторов, эффективно доказывающих корректность программ с рекурсией неограниченной глубины [1, 2, 3], работающих во многих ситуациях на порядок лучше аналогов. Общая их черта состоит в том, что они сводят задачу верификации кода к задаче автоматического доказательства теорем над системой дизъюнктов Хорна.
В докладе планируется кратко рассмотреть общие принципы работы таких верификаторов (пути к кодированию программ в систему дизъюнктов Хорна, алгоритмы поиска индуктивного инварианта и контрпримеров), а также некоторые продвижения докладчика в этой области (алгоритмы синхронизации дизъюнктов Хорна [4], адаптация символьного исполнения императивных программ для случая неограниченной рекурсии).
 
Материалы к докладу:
    1. Gurfinkel A. et al. The SeaHorn verification framework //International Conference on Computer Aided Verification. – Springer, Cham, 2015. – С. 343-361.
    2. Kahsai T. et al. JayHorn: A framework for verifying Java programs //International Conference on Computer Aided Verification. – Springer International Publishing, 2016. – С. 352-358.
    4. Mordvinov D., Fedyukovich G. Synchronizing Constrained Horn Clauses //LPAR, EPiC Series in Computing. EasyChair. – 2017.
 

29 сентября 2017
(пятница 17-00 каб. А.Н. Терехова)

Литвинов Юрий Викторович
Обзор школы LASER-2017

Школа LASER-2017 (https://www.laser-foundation.org/) проходила с 9 по 17 сентября на о. Эльба, темой школы этого года стало программное обеспечение в робототехнике. Школа проходила в формате коротких лекционных курсов (как правило, из 6 лекций), читавшихся видными представителями сообщества, приглашённого доклада Андрея Николаевича и небольшого количества студенческих презентаций. Лекции читали:
* Davide Brugali, University of Bergamo --- о линейках программных продуктов, feature-oriented анализе и его применении в робототехнике;
* Rodolphe Gelin, Softbank Robotics --- о человекоподобных роботах;
* Ashish Kapoor, Microsoft Research --- о безопасном управлении квадрокоптерами, вероятностных темпоральных логиках и симуляции;
* Nenad Medvidovic, University of Southern California --- об архитектуре ПО вообще и робототехнических систем в частности; 
* Bertrand Meyer, Politecnico di Milano --- о параллелизме и применении Eiffel в робототехнике; 
* Issa Nesnas, NASA Jet Propulsion Laboratory --- о робототехнике в космических исследованиях вообще и архитектуре бортового ПО роверов в частности; 
* Hiroshi “Gitchang” Okuno, Waseda University and Kyoto University --- о распознавании звука, локализации источников звука, разделении и анализе звуковых потоков, роли восприятия звука в человекомашинном взаимодействии.
В докладе будет рассказано об основных идеях и научных результатах, обсуждавшихся в рамках школы.

31 августа 2017
(четверг 17-00 каб. А.Н. Терехова)

Ханов Артур Рафаэльеаич
Безопасность смарт-контрактов в криптовалюте Ethereum

Ethereum - одна из наиболее быстроразвивающихся криптовалют. Она позволяет не только обмениваться денежными средствами. В ее основе лежат так называемые смарт-контракты. Это программы на особом языке, которые выполняются всей децентрализованной сетью и могут содержать достаточно сложную логику. Важнейшим аспектом развития Ethereum является ее безопасность. Поэтому программы-смарт-контракты необходимо уметь проверять на предмет того, насколько описанные в них условия устойчивы к атакам злоумышленника. Так год назад произошла история, в которой из-за уязвимого смарт-контракта злоумышленник чуть не украл более 50 миллионов долларов. Возможно ли ограничить логику работы контрактов таким образом, чтобы они были по-прежнему достаточно выразительны для написания и в то же время верифицируемы? Ответ на этот вопрос и предстоит получить участникам семинара.


Архив семинара

Заседания 2016/2017 учебного года

Заседания 2014/2015 учебного года

Заседания 2013/2014 учебного года

Заседания 2012/2013 учебного года

Заседания 2011/2012 учебного года

Заседания 2010/2011 учебного года

Заседания 2009/2010 учебного года

Действия с Документом