LLVM-based static analysis tool using type and effect systems. - Mikhail A. Belyaev; V. A. Tsesko (Autom. Control. Comput. Sci., 2012)

Software defect detection by combining bounded model checking and approximations of functions. - Marat Kh. Akhin; Mikhail A. Belyaev; Vladimir M. Itsykson (Autom. Control. Comput. Sci., 2014)

Using a bounded model checker for test generation: How to kill two birds with one SMT solver. - Maxim Petrov; Kirill Gagarski; Mikhail A. Belyaev; Vladimir M. Itsykson (Autom. Control. Comput. Sci., 2015)

Borealis Bounded Model Checker: The Coming of Age Story. - Marat Akhin; Mikhail A. Belyaev; Vladimir M. Itsykson (Present and Ulterior Software Engineering, 2017)

ReduKtor: How We Stopped Worrying About Bugs in Kotlin Compiler. - Daniil Stepanov; Marat Akhin; Mikhail A. Belyaev (ASE, 2019)

Type-Centric Kotlin Compiler Fuzzing: Preserving Test Program Correctness by Preserving Types. - Daniil Stepanov; Marat Akhin; Mikhail A. Belyaev (ICST, 2021)

Kotlin coroutines: design and implementation. - Roman Elizarov; Mikhail A. Belyaev; Marat Akhin; Ilmir Usmanov (Onward!, 2021)

Kex at the 2021 SBST Tool Competition. - Azat Abdullin; Marat Akhin; Mikhail A. Belyaev (SBST@ICSE, 2021)

Kex at the 2022 SBST Tool Competition. - Azat Abdullin; Marat Akhin; Mikhail A. Belyaev (SBST@ICSE, 2022)

Causal explicit algorithm for heat conduction in a plasma. - Mikhail A. Belyaev (Comput. Phys. Commun., 2024)