Predicate Analysis with BLAST 2.7 - (Competition Contribution). - Pavel Shved; Mikhail U. Mandrykin; Vadim S. Mutilin (TACAS, 2012)

Using linux device drivers for static verification tools benchmarking. - Mikhail U. Mandrykin; Vadim S. Mutilin; Evgeny Novikov; Alexey V. Khoroshilov; Pavel Shved (Program. Comput. Softw., 2012)

Experience of improving the blast static verification tool. - Pavel Shved; Vadim S. Mutilin; Mikhail U. Mandrykin (Program. Comput. Softw., 2012)

CPAchecker with Sequential Combination of Explicit-Value Analyses and Predicate Analyses - (Competition Contribution). - Stefan Löwe; Mikhail U. Mandrykin; Philipp Wendler (TACAS, 2014)

High-level memory model with low-level pointer cast support for Jessie intermediate language. - Mikhail U. Mandrykin; Alexey V. Khoroshilov (Program. Comput. Softw., 2015)

Configurable toolset for static verification of operating systems kernel modules. - Ilja S. Zakharov; Mikhail U. Mandrykin; Vadim S. Mutilin; Evgeny Novikov; Alexander K. Petrenko; Alexey V. Khoroshilov (Program. Comput. Softw., 2015)

Region analysis for deductive verification of C programs. - Mikhail U. Mandrykin; Alexey V. Khoroshilov (Program. Comput. Softw., 2016)

Towards deductive verification of C programs with shared data. - Mikhail U. Mandrykin; Alexey V. Khoroshilov (Program. Comput. Softw., 2016)

A Memory Model for Deductively Verifying Linux Kernel Modules. - Mikhail U. Mandrykin; Alexey V. Khoroshilov (Ershov Informatics Conference, 2017)

CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions - (Competition Contribution). - Pavel S. Andrianov; Karlheinz Friedberger; Mikhail U. Mandrykin; Vadim S. Mutilin; Anton Volkov (TACAS (2), 2017)

Deductive Verification of Unmodified Linux Kernel Library Functions. - Denis Efremov; Mikhail U. Mandrykin; Alexey V. Khoroshilov (ISoLA (2), 2018)

CPA-BAM-Slicing: Block-Abstraction Memoization and Slicing with Region-Based Dependency Analysis - (Competition Contribution). - Pavel S. Andrianov; Vadim S. Mutilin; Mikhail U. Mandrykin; Anton A. Vasilyev (TACAS (2), 2018)

Lemma Functions for Frama-C: C Programs as Proofs. - Grigoriy Volkov; Mikhail U. Mandrykin; Denis Efremov (CoRR, 2018)

Complete Decision Procedure for the Theory of Bounded Pointer Arithmetic. - R. F. Sadykov; Mikhail U. Mandrykin (Program. Comput. Softw., 2022)