For citations:

SADYKOV R.F., MANDRYKIN M.U. Complete decision procedure for the theory of bounded pointer arithmetic based on quantifier instantiation and SMT. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2021;33(4):177-194. (In Russ.) https://doi.org/10.15514/ISPRAS-2021-33(4)-13