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).
- 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
Borealis Bounded Model Checker: The Coming of Age Story
Marat Akhin, Mikhail Belyaev, Vladimir Itsykson
Using a Bounded Model Checker for Test Generation: How to Kill Two Birds with One SMT Solver
M. Petrov, K. Gagarski, M. Belyaev, V. Itsykson
Эффективное исполнение программного кода в контролируемом окружении как способ улучшения результатов статического анализа и верификации программ
М.А. Беляев, В.М. Ицыксон
Fast and Safe Concrete Code Execution for Reinforcing Static Analysis and Verification
M. Belyaev, V. Itsykson
Software Defect Detection by Combining Bounded Model Checking and Approximations of Functions
M. Akhin, M. Belyaev, V. Itsykson
Improving Static Analysis by Loop Unrolling on an Arbitrary Iteration
М. Belyaev, М. Akhin, V. Itsykson