Mikhail Belyaev

Born in 1988. Attended school at the Automation and Computer Systems dept in Saint-Petersburg State Polytechnic University in 2005. Graduated in 2011.

Since 2011 actively participates in the hardware & software development lab (aka Digitek Labs) projects as a researcher and developer. In 2015 a part of Digitek labs was remodeled as a part of JetBrains Research initiative into the Laboratory of Program Analysis and Verification (aka Vorpal Research).

Teaching courses since 2012. In 2014–2015 participated in ACM ICPC initiative of the university as a trainer.

Done three separate research internships at Microsoft Research Redmond (the RiSE group).


[bitbucket] [github] [linkedin]

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

Research interests

  • Software Engineering
  • Program Analysis and Verification
  • Formal Logic and Type Theory
  • Open Research Questions in the Area of Compilation and Debugging
  • Language Design



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.

Research Internships


Email: belyaev@kspt.icc.spbstu.ru

Address: Peter the Great St.Petersburg Polytechnic University, bldg. 9, room 301
Polytechnicheskaya st., 21, Saint-Petersburg, Russia