В статье дается обзор существующих методов верификации динамической памяти; проводится их сравнительный анализ; оценивается применимость для решения задач управления, контроля и верификации динамической памяти. Данная статья состоит из восьми разделов. Первый раздел - введение. Во втором обсуждаются проблемы управления динамической памятью. В третьем рассматривается исчисление Хоара. В четвёртом речь идёт о преобразованиях heap в стек. Пятый вводит понятие анализа образов динамической памяти. Шестой посвящен ротации указателей, седьмой - логике распределенной памяти. В последнем разделе рассматриваются возможные направления дальнейших научных исследований в данной области, в частности: распознавание на уровне записи различных экземпляров объектов; автоматизация доказательств; использование «горячего» кода, то есть программного кода, который сам себя обновляет при запуске программы; расширение интуитивности объяснений доказательств и другие. С. 5-30.

The article provides an overview of the existing methods of dynamic memory verification; their comparative analysis is carried out; the applicability for solving problems of control, monitoring, and verification of dynamic memory is evaluated. This article is divided into eight sections. The first section is an introduction, the second discusses dynamic memory management problems, the third discusses Hoare's calculus, the fourth considers heap transformations to stack, the fifth introduces the concept of dynamic memory image analysis, the sixth is dedicated to the rotation of pointers, the seventh is on the logic of distributed memory. The last section discusses possible directions of further research in this area; more specifically: recognition at recording level of various instances of objects; automation of proofs; “hot” code, that is, software code that updates itself when the program runs; expanding intuitiveness of proof explanations and others.