• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
Книга
ECPPM 2021 – eWork and eBusiness in Architecture, Engineering and Construction

Под науч. редакцией: Vitaly Semenov, R. J. Scherer.

CRC Press, 2021.

Статья
Optimization of ProVerif Programs for AKE Protocols

Vinarskii E., Демаков А. В.

Programming and Computer Software. 2022. Vol. 48. No. 8. P. 781-787.

Глава в книге
Adaptive Homing Sequences for Partial Weakly-initialized Observable FSMs

Vinarskii E., Твардовский А. С., Evtushenko N. V.

In bk.: Proceedings 2021 IEEE East-West Design & Test Symposium (EWDTS). IEEE, 2021.

Препринт
Preventive Model-based Verification and Repairing for SDN Requests

Burdonov I., Kossachev A., Nina Yevtushenko et al.

arxiv.org. Computer Science. Cornell University, 2020

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

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

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

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


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

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


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