- A
- A
- A
- АБB
- АБB
- АБB
- А
- А
- А
- А
- А
Адрес: 109028, г. Москва, Покровский бульвар, д. 11
Телефон: +7(495) 772-95-90*27297
Кафедра создана в 2015 году в структуре департамента программной инженерии на базе Института cистемного программирования им. В.П. Иванникова РАН (ИСП РАН).
Системное программирование – это основа программной инженерии (науки о производстве программ). Специализация кафедры охватывает ряд важнейших направлений: операционные системы, компиляторные технологии, технологии и инструменты разработки программ, системная интеграция и прикладные программные комплексы и др.
Под науч. редакцией: Vitaly Semenov, R. J. Scherer.
CRC Press, 2021.
Bresolin D., El-Fakih K., Villa T. et al.
Formal Methods in System Design. 2022.
Shutkin V., Morozkin N., Zolotov V. et al.
In bk.: ECPPM 2021 – eWork and eBusiness in Architecture, Engineering and Construction. CRC Press, 2021. P. 406-413.
Burdonov I., Kossachev A., Nina Yevtushenko et al.
arxiv.org. Computer Science. Cornell University, 2020
Николай Бьорнер - Открытая конференция ИСП РАН им. В.П. Иванникова 2019
5 декабря, 13:30 (СИНИЙ ЗАЛ). Николай Бьорнер выступит с пленарным докладом "От путеводных звезд к озарениям ума: как задачи большого размаха ведут за собой технологии автоматизированных доказательств".
Аннотация: Современные инструменты проведения доказательств (пруверы) уже 10 лет демонстрируют невероятные возможности, снискавшие для них бесчисленные практические применения. Построение прувера требует проведения бесчисленных экспериментов, аккуратно спланированных, поддержанных нетривиальными наблюдениями и глубоким пониманием теории доказательства и логических формализмов. В докладе я описываю результат, за последние годы многократно применённый в ядре решателя Z3 в разных обличьях: поиск и насыщение на основе моделей. Z3 – известный промышленный решатель и прувер, разрабатываемый в Microsoft Research. Вдохновение не рождается на пустом месте.
Путеводные звезды для него были взяты из разных задач: верифицируемых компиляторов, символьного выполнения, квантовых вычислений и верификации сетей и др. Эти маяки определили направления исследований и разработки компонентов Z3.
6 декабря, 10:00 (СИНИЙ ЗАЛ). Николай Бьорнер проведет Практический Семинар: Программирование в ограничениях с помощью Z3
Аннотация: Многие вопросы верификации, анализа, тестирования и синтеза программ сводятся к определению совместности логических формул. Однако, есть и задачи, в которых совместность даже с доказывающей ее моделью недостаточна. Примерами полезной дополнительной информации являются интерполянты, модели, удовлетворяющие некоторому критерию оптимальности, стратегии решения формул с кванторами, перечисление и подсчет решений. В данном иллюстративном докладе демонстрируются упомянутые логические сервисы (с помощью Jupyter) с точки зрения SMT-решателя Ζ3.
Если вы планируете посетить данное мероприятие, необходимо зарегистрироваться:
https://isprasopen.ru/#Registration