Mikhail Belyaev

Mikhail Belyaev

Research Groups


Mikhail graduated from the St. Petersburg Polytechnic University in 2011, and since then has been involved in various R&D projects. He took three separate internships at Microsoft Research Redmond.

Known as a language collector, Mikhail claims to be proficient in ~10 programming languages, which is: a). obviously not true, and b). not enough these days anyway.

Mikhail teaches programming basics (Java/C++), functional programming (Haskell & friends), software engineering (project management, teamwork), and software QA (static analysis, type systems, etc).

Professional Activity

Current Research

  • Mainly working on Borealis — the bounded model checker for C


  • MSR Redmond, 2013 (feat. Nikolai Tillmann) — adding debugging experience to the Touchdevelop project (visual debugger, crash logs cloud processing, instrumentation, etc.)
  • MSR Redmond, 2014 (feat. Tom Ball & Ella Bounimova) — "verifying the verifier", developing a framework for testing, checking and visualizing rules for SLIC, a static verifier rule definition language
  • MSR Redmond, 2015 — turning the SLIC framework into a production-ready tool, expanding the volume of supported rules from 10% to 99%

More info can be found here


ReduKtor: How We Stopped Worrying About Bugs in Kotlin Compiler


Daniil Stepanov, Marat Akhin, Mikhail Belyaev

ASE 2019

Read more

Borealis Bounded Model Checker: The Coming of Age Story

September 2017

Marat Akhin, Mikhail Belyaev, Vladimir Itsykson

Present and Ulterior Software Engineering (pp. 119--137)

Read more

Using a Bounded Model Checker for Test Generation: How to Kill Two Birds with One SMT Solver

December 2015

M. Petrov, K. Gagarski, M. Belyaev, V. Itsykson

Automatic Control and Computer Sciences, Volume 49, Issue 7

Read more

Эффективное исполнение программного кода в контролируемом окружении как способ улучшения результатов статического анализа и верификации программ


М.А. Беляев, В.М. Ицыксон

Моделирование и анализ информационных систем

Read more

Fast and Safe Concrete Code Execution for Reinforcing Static Analysis and Verification


M. Belyaev, V. Itsykson


Read more

Software Defect Detection by Combining Bounded Model Checking and Approximations of Functions

December 2014

M. Akhin, M. Belyaev, V. Itsykson

Automatic Control and Computer Sciences, Volume 48, Issue 7

Read more

Improving Static Analysis by Loop Unrolling on an Arbitrary Iteration


М. Belyaev, М. Akhin, V. Itsykson

Humanities and Science University Journal, #8

Read more