• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Статья
“Statistical and Combinatorial Analysis of the TOR Routing Protocol - Structural Weaknesses Identified in the Tor Network”

Filiol E. A., Delong M., Job N.

FORSe 2018 & 2019 Special Issue, Antonella Santone Guest editor, Journal of computer Virology and Hacking Techniques. 2020. Vol. 16. No. 1. P. 3-18.

Глава в книге
Effective Scheduling of Strict Periodic Task Sets with Given Permissible Periods in RTOS

Zelenov S. V., Zelenova S. A.

In bk.: Lecture Notes in Computer Science. Vol. 11964: Perspectives of System Informatics. Springer, 2019. P. 214-222.

Препринт
Темпоральные расширения в стандарте SQL

С.Д. Кузнецов

Препринты ИСП РАН. Институт системного программирования им. В.П. Иванникова РАН, 2017. № 30.

Николай Бьорнер - Открытая конференция ИСП РАН им. В.П. Иванникова 2019

Несколько дней осталось до начала работы Открытой конференции ИСП РАН им. В.П. Иванникова. В этом году мероприятие посвящено 25-летию Института. Ожидается много гостей, среди которых Николай Бьорнер - главный научный сотрудник Microsoft Research, (Редмонд, США).

5 декабря, 13:30 (СИНИЙ ЗАЛ). Николай Бьорнер выступит с пленарным докладом "От путеводных звезд к озарениям ума: как задачи большого размаха ведут за собой технологии автоматизированных доказательств".

Аннотация: Современные инструменты проведения доказательств (пруверы) уже 10 лет демонстрируют невероятные возможности, снискавшие для них бесчисленные практические применения. Построение прувера требует проведения бесчисленных экспериментов, аккуратно спланированных, поддержанных нетривиальными наблюдениями и глубоким пониманием теории доказательства и логических формализмов. В докладе я описываю результат, за последние годы многократно применённый в ядре решателя Z3 в разных обличьях: поиск и насыщение на основе моделей. Z3 – известный промышленный решатель и прувер, разрабатываемый в Microsoft Research. Вдохновение не рождается на пустом месте.
Путеводные звезды для него были взяты из разных задач: верифицируемых компиляторов, символьного выполнения, квантовых вычислений и верификации сетей и др. Эти маяки определили направления исследований и разработки компонентов Z3.


6 декабря, 10:00 (СИНИЙ ЗАЛ). Николай Бьорнер проведет Практический Семинар: Программирование в ограничениях с помощью Z3

Аннотация: Многие вопросы верификации, анализа, тестирования и синтеза программ сводятся к определению совместности логических формул. Однако, есть и задачи, в которых совместность даже с доказывающей ее моделью недостаточна. Примерами полезной дополнительной информации являются интерполянты, модели, удовлетворяющие некоторому критерию оптимальности, стратегии решения формул с кванторами, перечисление и подсчет решений. В данном иллюстративном докладе демонстрируются упомянутые логические сервисы (с помощью Jupyter) с точки зрения SMT-решателя Ζ3.


Если вы планируете посетить данное мероприятие, необходимо зарегистрироваться:
https://isprasopen.ru/#Registration