About me

Who am I?

My name is Mikhail and I write stuff, program stuff and teach stuff. In particular, I teach university students and do things for Jetbrains Research at the program analysis and verification lab.

I also know stuff about program analysis and verification, quite a number of programming languages and software engineering in general. Right now I’m quite fixed on Kotlin and stuff around it.

What is this site for?

Mostly for long-writes in English that don’t fit into a tweet. Technical notes, Kotlin stuff, my thoughts on programming, life and everything.

What is this site not for?

My personal thoughts and feelings on non-technical stuff. I have other social media for that. This may change in the future.

What do I do?

Quite a number of things, actually.


Well, this site.
Also, currently writing the Kotlin language specification (WIP).


  • Theory:
    • Functional programming (at Peter the Great St. Petersburg Polytechnic University)
    • Program analysis 101 (at Higher School or Economics/Academic University)
  • Practice:
    • Programming basics (C/C++/Java/Kotlin)
    • Software engineering
  • Diploma projects:
    • Type classes for Kotlin by Eugine Khandygo
    • Transpiling C++11/14 code back to C++03 by Yuliy Illarionov
    • Pattern matching for Kotlin by Sergei Vorobyov
    • Variadic generics for Kotlin by Pavel Kirphichenkov


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

Selected publications:

Akhin M.Kh., Belyaev M.A., Itsykson V.M.,
Borealis Bounded Model Checker: The Coming of Age Story
PAUSE 2017, pp. 119-137

Belyaev M.A., Itsykson V.M.,
Fast and safe concrete code execution for reinforcing static analysis and verification
Modeling and Analysis of Information Systems 2015, 60 (6), pp. 763–772

Petrov M.A, Gagarski K.A., Belyaev M.A., Itsykson V.M.,
Using a bounded model checker for test generation: How to kill two birds with one SMT solver.
Automatic Control and Computer Sciences 2015, 49 (7), pp. 466–472

Akhin M.Kh., Belyaev M.A., Itsykson V.M.,
Software defect detection by combining bounded model checking and approximations of functions
Automatic Control and Computer Sciences 2014, 48 (7), pp. 389–397

Belyaev M.A., Akhin M.Kh., Itsykson V.M.,
Improving static analysis by loop unrolling on arbitrary iteration
(the attached pre-publishing version has a different name)
University Scientific Journal 2014, 8, pp. 154–168

Belyaev M.A., Gaivoronski S.A.,
Towards load balancing in SDN-networks during DDoS-Attacks
2014 MoneTEC proceedings