ABSTRACT DATA TYPES FOR DYNAMIC MEMORY SIMULATION
Keywords:pointer analysis, alias calculus, separation logic, dynamic memory, verification, program analysis, verifying translator
The article describes formal-conceptual approaches for representing knowledge by introducing new abstract data types and pointers, and also discusses the current directions of studying pointer analyzes and open problems that have arisen over the long history of the development of this field. A comparative analysis of pointers (pointer analysis) has been carried out, which allows judging the correctness of programs, or rather, its correct handling of dynamic memory, and also improves its performance. A brief description of two methods for analyzing pointers - Calculus of Aliasing and Separation Logic - is given, the subsequent development of the alias calculus is presented, and the MoRe programming language, its formal syntax and structural operational semantics are developed. The proof of the correctness of algorithms for syntactic checking of programs with analysis of pointers in solving the problem for the logic of separation, for any distribution of aliases is given.