Mikhail Belyaev


Mikhail graduated from the St. Petersburg Polytechnic University in 2011, and since then has been involved in various R&D projects here and there. 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 does some teaching in 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


  • Borealis Static Analysis System for C
  • Kotlin Online Education Platform