Беляев Михаил Анатольевич
Родился в 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: >>
Области научных интересов:
- Программная инженерия
- Анализ и верификация ПО
- Теория типов и формальные логики
- Научные вопросы в рамках средств компиляции, верификации и отладки
Принимает участие в преподавании курсов:
- Теория и технологии программирования (C++)
- Теория и технологии программирования (Java)
- Технологии разработки ПО
- Языки функционального программирования
- Методы обеспечения качества ПО
Публикации
| — | — | — |
|---|---|---|
| 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
