English

Беляев Михаил Анатольевич

Родился в 1988 году. В 2005 году поступил на кафедру автоматики и вычислительной техники СПбГПУ. В 2011 году окончил магистратуру той же кафедры (сейчас — кафедра компьютерных систем и программных технологий).

С 2011 года занимается разработкой и исследованиями в рамках лаборатории программно-аппаратных разработок Digitek Labs, с 2015 года — лаборатории верификации и анализа ПО (совм. с компанией JetBrains).

C 2012 года занимается преподавательской деятельностью на кафедре. В 2014-2015 годах участвовал в организации занятий для команд института по спортивному программированию.

Трижды проходил стажировки в Microsoft Research Redmond в научной группе Research in Software Engineering. Имеет опыт разработки крупных и средних проектов на более чем 10 языках программирования. Активно занимается разработкой собственных библиотек.

Ссылки

[bitbucket] [github] [linkedin]

Scopus ID: 7003903519 >>
ORCID: 0000–0003–1260–9211 >>
SPIN: 8235–4265 >>
Google Scholar: >>

Области научных интересов:

  • Программная инженерия
  • Анализ и верификация ПО
  • Теория типов и формальные логики
  • Научные вопросы в рамках средств компиляции, верификации и отладки

Принимает участие в преподавании курсов:

Публикации

Borealis bounded model checker: the coming of age story Akhin, M., Belyaev, M., Itsykson, V Present and Ulterior Software Engineering. 2017. pp. 119–137
Fast and safe concrete code execution for reinforcing static analysis and verification Belyaev M., Itsykson V. Моделирование и анализ информационных систем. 2015. 60 (6), pp. 763–772
Using a bounded model checker for test generation: How to kill two birds with one SMT solver. Petrov, M., Gagarski, K., Belyaev, M., Itsykson, V. Automatic Control and Computer Sciences. 2015. 49 (7), pp. 466–472
Software defect detection by combining bounded model checking and approximations of functions Akhin M., Belyaev M., Itsykson V. Automatic Control and Computer Sciences. 2014. 48 (7), pp. 389–397
Towards load balancing in SDN-networks during DDoS-Attacks Belyaev, M., Gaivoronski, S. 2014 MoneTEC proceedings
Использование метода ограниченной проверки моделей для генерации тестов Петров М.А., Гагарский К.А., Беляев М.А., Ицыксон В.М. Моделирование и анализ информационных систем. 2014. Т. 21. № 6. С. 83–93.
Improving static analysis by loop unrolling on an arbitrary iteration Belyaev M.A., Akhin M., Itsykson V.M. Университетский научный журнал. 2014. № 8. С. 154–168.
Обнаружение дефектов в программном обеспечении путем объединения ограниченной проверки моделей и аппроксимации функций Ахин М.Х., Беляев М.А., Ицыксон В.М. Моделирование и анализ информационных систем. 2013. Т. 20. № 6. С. 22–35.
LLVM-based static analysis tool using type and effect systems Belyaev, M., Tsesko, V. 2012 Automatic Control and Computer Sciences 46 (7), pp. 324–330
Статический анализ с использованием систем типов и эффектов на основе LLVM Беляев М.А., Цесько В.А. Моделирование и анализ информационных систем. 2011. Т. 18. № 4. С. 45–55.

Научные стажировки

  • 2013 — MSR Redmond. Разработка отладочной инфраструктуры в проекте Microsoft Touchdevelop. Руководитель — Nikolai Tillmann.
  • 2014 — MSR Redmond. Разработка инфраструктуры для верификации, трансформации и визуализации правил для системы SDV/XDV. Руководитель — Ella Bounimova
  • 2015 — MSR Redmond. Применение разработанной инфраструктуры ко всему массиву правил SDV/XDV. Руководитель — Ella Bounimova

Контакты

Email: belyaev@kspt.icc.spbstu.ru

Адрес: 9 учебный корпус СПбПУ, комната 301